I'm going to teach a course on implementing dependently typed programming languages at @monadic_waw this June! If you have any questions you'd like to see covered, feel free to ask. The 6 hours of videos will be posted online.
-
-
Replying to @tangled_zans
I have a question! Is there a difference between type-checking and running a program in a dependently typed language?
1 reply 0 retweets 3 likes -
Replying to @andrejbauer
I feel like I'm being tested :D no, because we need to evaluate the program in order to be able to check that two types are equal
1 reply 0 retweets 1 like -
-
Replying to @andrejbauer @tangled_zans
In Idris some things are on the type level (ie. you can verify that a vector has n elements), but not the program as a whole. So the type-level bits are evaluated at compilation time, but not the program itself.
1 reply 0 retweets 1 like -
Replying to @monadic_party @tangled_zans
Yes yes.
@edwinbrady is a hacker at heart.1 reply 0 retweets 1 like -
Replying to @andrejbauer @tangled_zans
I am indeed. But i don't think that's the point here - the evaluation/execution distinction is an important one, as
@tangled_zans said earlier.1 reply 0 retweets 4 likes
Idris 2, being QTT based, has another way of looking at it: IO a is a wrapper for 1 World -> (a, World). It's fine to evaluate that at compile time since the World doesn't get instantiated until run time.
-
-
Replying to @edwinbrady @tangled_zans
1 World → (a, World) looks a lot like a comodel to me. Will Idris 3 have kernel and user modes?
0 replies 0 retweets 1 likeThanks. 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.