steshaw (13) [Avatar] Offline
#1
The book mentions that = is built into Idris syntax since = is a reserved symbol. Is this the only reason that "Equality in General" is built-in? Are there other pros/cons to having = built-in?

Following listing 8.4 but with an explicit argument, the following seems to work on some simple examples:

data Equal : a -> b -> Type where
  Reflexive : (x : a) -> Equal x x

I was also a little surprised to see that b there (after EqNat with two Nats). i.e. a and b can be different types. Is this something to do with heterogenous equality and/or John-Major equality (which I've heard of but don't grok yet)?

I also tried the following which worked equally well on my simple examples:

data Equal : a -> a -> Type where
  Reflexive : (x : a) -> Equal x x
Edwin Brady (65) [Avatar] Offline
#2
The only thing that's built in in practice is the syntax. Your definition of 'Equal' would work perfectly fine, and in fact that's how (=) is defined internally.

The reason for the different 'a' and 'b' is that it lets you say things like: `(xs : Vect n a) -> (ys : Vect m a) -> xs = ys -> x :: xs = y :: ys`, that is, talk about equalities between dependent types.
steshaw (13) [Avatar] Offline
#3
That's great, thanks. I've been trying to understand the underlying type theory. AIUI, some variant of MLTT comes with equality types baked in but it seems that Idris' TT comes with inductive data types built in that you can build equality types from. Would you recommend to read Luo's "Computation and Reasoning" book or is there a better resource for Idris TT (which I understand from your implementation paper is basically UTT)? Perhaps just the TT.hs?

I've heard of mention of heterogenous equality (which I think is known as John-Major equality). Is this why Eq is defined the way it is in Idris?
Edwin Brady (65) [Avatar] Offline
#4
Luo's book is really good for the background, though I wouldn't say it's an easy read! The one thing that might be a bit mysterious about the Idris type theory is that it has pattern matching definitions built in, using a special kind of binding for the pattern variables. This is basically what the implementation paper talks about and it might help to try to read that alongside the TT.hs source.

The equality type in Idris is indeed a heterogeneous equality (which we used to call "John Major" equality when he was better known smilie). I think this is in most cases the less surprising choice, when programming.
steshaw (13) [Avatar] Offline
#5
I tend to get a bit demotivated when things are too much of a hard read so I think I'll hold off on Luo's book for now. I'll certainly re-read your paper alongside the code for TT. I've been wondering how hard it might be to get WHNF going. There's a mysterious file called WHNF.hs...
Edwin Brady (65) [Avatar] Offline
#6
I need to make WHNF work for more efficient type checking (that is, only evaluating as much as is needed). I'll do that pretty soon, probably working along the lines of the current evaluator. The current implementation of WHNF in WHNF.hs works, but is pretty slow, so I haven't dropped it in anywhere yet.