You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is probably roughly the same bug as #35, but as it does not involve recursive HITs, I am creating a separate issue.
It is possible to create a path p:Path T a b such that p@1 does not reduce to b:
module bug where
import prelude
A:U=undefined
B:U=undefined
f:A->B=undefined
opaque A -- to print #A instead of undefined
opaque B
opaque f
data HIT
= iA (_:A)
| iB (_:B)
| gl (x:A) <i>
[ (i=0) -> iA x
, (i=1) -> iB (f x)
]
x : A = undefined
opaque x
p1 : HIT = transport (<_> HIT) (gl {HIT} x @ 1)
p : Path HIT
(transport (<_> HIT) (gl {HIT} x @ 0))
p1
= <r> transport (<_> HIT) (gl {HIT} x @ r)
p1 reduces to hComp HIT (iB (comp (<_> B) (f x) [])) [], but p@1 reduces to hComp HIT (iB (f (comp (<_> A) x []))) [].
However, this works:
p : Path HIT
(transport (<_> HIT) (gl {HIT} x @ 0))
p1
= <r> comp (<_> HIT) (gl {HIT} x @ r)
[(r=0)-><i> fill (<_> HIT) (iA x) [] @ i
,(r=1)-><i> fill (<_> HIT) (iB (f x)) [] @ i
]
Maybe the definition of composition for a path constructor should depend on its system ?
The text was updated successfully, but these errors were encountered:
Should p1 and p@1 both reduce to just hComp HIT (iB (f x)) []?
I think that for a HIT with no parameters, transps/squeezes should not be applied at all to constructor arguments in transpHIT/squeezeHIT. I have attempted to fix this special case with this hack, provided without warranty of any kind: https://gist.github.com/tomjack/da36301ceb1d97c73aa15731332d0636
This is probably roughly the same bug as #35, but as it does not involve recursive HITs, I am creating a separate issue.
It is possible to create a path p:Path T a b such that p@1 does not reduce to b:
p1 reduces to
hComp HIT (iB (comp (<_> B) (f x) [])) []
, but p@1 reduces tohComp HIT (iB (f (comp (<_> A) x []))) []
.However, this works:
Maybe the definition of composition for a path constructor should depend on its system ?
The text was updated successfully, but these errors were encountered: