[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers

[Richard Eisenberg]

More good questions.

On Jun 9, 2013, at 10:20 PM, TP wrote:

> In fact the extension ScopedTypeVariables is not needed to make your version 
> work. However, if I extend a bit your version like that:
> 
<snip>

> So I don't understand why ScopedTypeVariables is needed in one case and not 
> in the other.
> 

This is because my code was (unintentionally) slightly redundant.

Here is the relevant code:

instance MkSNat n => MkSNat (Succ n) where
   mkSNat _ = SSucc (mkSNat ???)

What could possibly go in `???`? As in, what is the required type of that expression? We know
mkSNat :: forall m. MkSNat m => Proxy m -> SNat m
and
SSucc :: forall m. SNat m -> SNat (Succ m)

Here, we are defining an instance of mkSNat where we know a bit more about its type. This instance of mkSNat must have type (Proxy (Succ n) -> SNat (Succ n)). (I'm just substituting in the (Succ n) from the instance header.) So, that means that the call to SSucc in the body of mkSNat must return a SNat (Succ n), which in turn means that its argument (mkSNat ???) must have type SNat n. Thus, in turn, the argument to that mkSNat must have type Proxy n. Because all of these inferences are sound and forced (i.e., there is no other choice for the type of ???), you can just put a `P` there, and GHC will do the right (and only possible) thing. So, without ScopedTypeVariables, the n that you would put on your annotation is totally unrelated to the n in the instance header, but this is benign because GHC can infer the type anyway. With ScopedTypeVariables, the `n`s are the same, which luckily agrees with GHC's reasoning, so it's all OK.

> 
> However, why am I compelled to put a constraint in 
> 
> ---------------
> instance MkSNat o => Show (Tensor o) where
>    show Tensor { order = o, name = str } = str ++ " of order "
>            ++ (show (mkSNat (P :: Proxy o)))  --- (*1*)
> ---------------
> ?


There are two good reasons:

1) You are suggesting that GHC do the following analysis:
- There is an instance for MkSNat Zero.
- Given an instance for MkSNat n, we know there is an instance for MkSNat (Succ n).
- Thus, there is an instance for every (n :: Nat).
This is precisely the definition of mathematical induction. GHC does not do induction. This could, theoretically, be fixed, though, which brings us to reason #2:

2) Class constraints are *runtime* things. This piece was a complete surprise to me when I first saw it, but it makes wonderful sense. One important property of Haskell is that it supports what is called "type erasure". Though the types are indispensable at compile-time, we have no need for them at runtime and can operate much faster without them. So, after type checking everything, GHC throws out the types. A consequence of type erasure is that a running program cannot make a decision based on a type. But, this conflicts with common knowledge: class methods are chosen based on types! The answer is that class constraints are *not* types. When you put, say, a (Show a) constraint on a function, you are really putting on an extra, implicit parameter to that function. This implicit parameter is a data structure that contains (pointers to) the specific implementations of the Show methods of type `a`. Thus, when you call `show`, that call compiles to a lookup in that data structure for the correct method. These data structures are called "dictionaries". 

In effect, when you put the "MkSNat o" constraint on your instance, you are saying that we must know the value of "o" at *runtime*. This makes great sense now, because we really do need to know that data at runtime, in order to print the value correctly. Thinking of dictionaries, the dictionary for Show for Tensors will contain a pointer to the correct dictionary for MkSNat, which, in turn, encodes the value of "o". In a very real way, MkSNat and SNat are *the same data structure*. MkSNats are implicit and SNats are explicit, but otherwise, they contain exactly the same data and have exactly the same structure.

And, no, this issue is unrelated to the openness of type classes.


Though I promised myself I wouldn't post about it again on this list, it's too germane to the discussion not to: You may be interested in the paper I co-wrote last year on singletons and their implementation in GHC. You can find the paper here: http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf   A lot of the issues that you're asking about are discussed there. And, in MkSNat, you've already reinvented some of what's in there (I called MkSNat "SingI", because it Introducces a singleton).

Richard