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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
