@pigworker What would an incomplete program with a hole in it do when executed?
-
-
Replying to @BrandonBloom
@BrandonBloom Dependently typed languages do partial evaluation of holey programs all the time. They get stuck in informative ways.1 reply 0 retweets 2 likes -
Replying to @pigworker
@pigworker I've tinkered w/ Mathematica a fair amount. In my xp the partial eval strategy works out 1/2 the time and blows up the other 1/2.1 reply 0 retweets 0 likes -
Replying to @BrandonBloom
@pigworker But either way, it's an interactive solution (which we need, don't get me wrong), but doesn't address production public API needs2 replies 0 retweets 0 likes -
Replying to @BrandonBloom
@pigworker Considering the sum-type constructor question, seems like I'd want to be able to annotate the type with a caller patch strategy.2 replies 0 retweets 0 likes -
Replying to @BrandonBloom
@BrandonBloom Sure. "Here's my new constructor. Here's how to try to fill the holes it creates. Call me if there are any tricky cases."1 reply 0 retweets 1 like -
Replying to @pigworker
@pigworker Right. I'd like to see more of that sort of thing.3 replies 0 retweets 0 likes -
Replying to @BrandonBloom
@BrandonBloom Basically, dependently typed programming can be MADDENING unless you make it easy to fiddle with datatype definitions.1 reply 1 retweet 1 like -
Replying to @pigworker
@pigworker I've tried to write basic programs in Idris multiple times & failed, hard. Told@edwinbrady the same thing at strange loop.3 replies 0 retweets 0 likes -
Replying to @BrandonBloom
@BrandonBloom@edwinbrady Many people make logically correct but pragmatically complicated type definitions, then complain it's too hard.2 replies 3 retweets 2 likes
@pigworker @BrandonBloom not much has been written (to my knowledge) on how to design types in the first place. A shame, since it's vital!
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.