Added a primitive composition for Id types which reduces with refl on… #71
Conversation
examples/idcomp.ctt
Outdated
| -- [ (i = 0) -> <_> a | ||
| -- , (i = 1) -> <_> a | ||
| -- , (j = 0) -> <_> a | ||
| -- , (j = 1) -> <_> a ]) [] |
There was a problem hiding this comment.
The indentation seems to be off by one here?
There was a problem hiding this comment.
Yep, this is a tabs vs spaces issue. They look aligned in my emacs buffer! Fixed now.
There was a problem hiding this comment.
And this is why one should never use tabs :)
examples/idcomp.ctt
Outdated
| -- refl | ||
| -- a -------> a | ||
| -- refId | | refId | ||
| -- . id1 | | . id2 |
There was a problem hiding this comment.
I am again nitpicking, but I have a feeling that you want the dot . before id1 to be aligned with f.
|
Wow! I have to say that the accompanying file |
Eval.hs
Outdated
| rs = unionSystem | ||
| (unionSystem | ||
| (border (q @@ (Atom i :/\: Atom j)) ps) | ||
| (border (p @@ (Atom i :/\: NegAtom j)) qs)) |
Eval.hs
Outdated
| idComp :: Val -> Val -> Val -> Val -> Val -> Val -> Val | ||
| idComp a u v w pId qId = case (pId, qId) of | ||
| (VIdPair p ps, qId) | eps `member` ps -> qId | ||
| (pId, VIdPair q qs) | eps `member` qs -> pId |
There was a problem hiding this comment.
Are these two cases really needed? Isn't it possible to get the next case to cover them?
There was a problem hiding this comment.
I would guess @IanOrton just wanted to take some shortcuts here?
There was a problem hiding this comment.
They seem a little dangerous to me, and if I comment them out the examples doesn't go through (even if one fixes the bug I found).
There was a problem hiding this comment.
Hmmm, I'm not sure. I think that they are needed to make sure that refl . p will reduce even when p is just a variable. To hit the other case you need to know that p is in fact a VIdPair. The behaviour should agree when the cases overlap so I've now moved these two cases after the third one. But maybe this behaviour is too strong? Do we want refl . p to reduce in the case when p is an undetermined variables of type Id A a b?
| in | ||
| VIdPair (VPLam i (comp j a v rs)) (joinSystem (border ps qs)) | ||
| (VIdPair p ps, qId) | eps `member` ps -> qId | ||
| (pId, VIdPair q qs) | eps `member` qs -> pId |
There was a problem hiding this comment.
I'm still a bit unsure about these two reduction rules. It seems dangerous to add them, but I don't have any concrete evidence why.
@simhu : Maybe you have more thoughts about this?
There was a problem hiding this comment.
As some justification, imagine that face formulae were first class objects and we could see that Id types were pairs of a path and a face formula. Then, using eta for pairs and paths, we would have:
idComp (<i> a , 1) qId
= idComp (<i> a , 1) (qId.1 , qId.2)
= (<i> comp j A [ 1 -> qId.1 @ (i /\ j) , qId.2 \/ (i=0) -> a ] a , 1 /\ qId.2)
= (<i> qId.1 @ i , qId.2)
= (qId.1 , qId.2)
= qId
… either side