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

[TP]

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