The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

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 (66) [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 (66) [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 (66) [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.