Richard Eisenberg wrote:
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 becau se 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.
Thanks Richard, it is perfectly clear.
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:
Ok, I imagine there is no general need for induction in GHC, otherwise it would already be implemented.
2) Class constraints are *runtime* things. This piece was a complete [...] 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.
"Type erasure" is a very interesting thing I did not know. But I am not sure to understand correctly the fact that class constraints are runtime things and why (I know C so I know what is a pointer, but I would need to go into the details). Anyway, if it is clear that GHC does not induction, then I can accept without problem that I am compelled to indicate the class constraint `MkSNat o =>` to GHC, such that the call of mkSNat on a value `P` of type `Proxy o` is correct from a type point of view - I imagine this is the way most people in Haskell community think about class constraints (?).
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).
I have read the beginning of the paper: very interesting. In particular the inequality at type level may be interesting for what I have to code. I will try to go on in the next days. In fact I already read about this possibility last month, but I stopped rapidly because I found this: http://hackage.haskell.org/trac/ghc/ticket/4385 http://hackage.haskell.org/trac/ghc/attachment/ticket/4385/Ticket.hs The answer of diatchki is not so hopeful, this suggests that there is a limit to computations at type-level. In my home project, I could code everything with a simple constructor of type `Tensor` (not `Tensor order`) and runtime checks, but encoding information in types makes certainly the code shorter (even if more difficult to read for many people) and safer, perhaps quicker if the runtime checks take time (I have heard from a colleague that the runtime checks of size when indexing a vector, case with which you deal at the beginning of your paper, took a lot of time in one of his C++ program - it is interesting to see how you dealt with this problem). It is a lot of efforts for me to learn all these advanced Haskell techniques that are not in textbooks, but I feel it is important: I try to summarize all what I learn in a LyX file. My hope is at the end to be able to code clean and efficient code in real programs, instead of script-like Python code with so many errors at runtime (this is what I do at work these days in a scientific computing company). I think also that for serious programs (say, order of magnitude 10^4 lines), it is necessary to have types (I would not use Haskell for a small script, of course). I feel also, from my coding experience, that states are a real problem in traditional C/C++/Python/... code, and I want to give a try with Haskell, monads, perhaps arrows, reactive programming, etc. Very interesting, but time-consuming. Still a long path to go for me. Thanks, TP