Coersion in strict data types and Omega1(S1). #250
Conversation
| * correction system, so it is not so bad. | ||
| * | ||
| * `Up _`: perhaps we can have nghcom? *) | ||
| | Ext _ | Univ _ | FHCom _ | V _ | Data _ | Up _ -> |
There was a problem hiding this comment.
We need a neutral hcom or a neutral ghcom so that a potential eliminator knows how to deal with it.
| auto | ||
|
|
||
| let winding-test/50 : Path int int/50 (winding (loopn int/50)) = | ||
| auto |
There was a problem hiding this comment.
Does anyone miss this? I can put it back...
There was a problem hiding this comment.
Let's keep it, just to make sure we do my introduce some really bad performance degradation. We could even move to different file if you felt it was clutter
|
@favonia when you run the 50th winding number on your machine, what happens? Travis seems to time out after 10 minute 😦 |
|
Glad that we kept the speed test. I apparently screwed up something. |
|
@favonia Laziness is notoriously difficult to predict 😆 I wonder if some change caused a bad thunk to get forced... |
|
Sorry. Please forget about the above comment (if it still showing in your browser). I probably found the actual cause. |
| @@ -17,18 +17,35 @@ let loopn (n : int) : Path s1 base base = | |||
| | pos n ⇒ | |||
| elim n [ | |||
| | zero ⇒ auto | |||
| | suc (n ⇒ loopn) ⇒ trans s1 (λ i → loop i) loopn | |||
| | suc (n ⇒ loopn) ⇒ trans s1 loopn (λ i → loop i) | |||
There was a problem hiding this comment.
This line and the similar line below seem to be causing the trouble.
There was a problem hiding this comment.
Heh.. So the issue is that when it associates in one way it is fast, and in the other way infeasible? That's very interesting.
There was a problem hiding this comment.
It somewhat makes sense. I changed the order to make the lemma easier to prove. The new one produces isuc from the outside and is perfect for induction.
There was a problem hiding this comment.
Shall we try a harder version of the lemma? I guess analogous to tail recursive function
There was a problem hiding this comment.
This performance asymmetry also exists in cubicaltt, btw.
There was a problem hiding this comment.
I guess to prove the "fast" version, it will take some gnarly coercion. Sadly, the goals are tens of thousands of lines long, so it's a little hard to tell what needs to be done.
There was a problem hiding this comment.
@favonia Can you elaborate on why it makes sense? I guess the performance of coe in fcom depends more on the complexity of the tubes than that of the cap?
There was a problem hiding this comment.
@ecavallo I am not sure. I have to think harder.
|
@jonsterling BTW, since we have parameters now, are you treating something like |
This reverts commit bbd1b84.
|
We decided to give up the speed test for now. |
favonia
dismissed
jonsterling’s stale review
Jon was then brainwashed by @faovonia.
Close #241.