The links to the paper itself seem broken
-
-
-
Just checked, it's definitely there...
- 4 more replies
New conversation -
-
-
That's a shame. Did you get useful feedback?
-
One very useful thing, which is that I can quite easily extend one example to really show the power of dependent/linear types. I just wish they'd also suggested what to take out to make room for it! But I'll manage to work that out for the next submission...
End of conversation
New conversation -
-
-
I found it surprising that metavariables (such as the `n` in the first Vec example) are not automatically promoted from 0 when used. Would that sort of analysis/auto-promotion produce other issues?
-
It is valuable to be able to say "this argument must not be used". Idris 1 does something a bit like that - erasure inference - and you can accidentally end up with big proof objects in your program.
End of conversation
New conversation -
-
-
it the https://www.type-driven.org.uk/papers/idris2.pdf … link dead? (yet, https://www.type-driven.org.uk/edwinb/papers/idris2.pdf … is working)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
"Abstract: Dependent types allow us to express precisely what a function is intended to do" - doesn't the code already describe exactly what the function does, why express it again in the type? cheeky_mode(off)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Too long? Looks good.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.