"Type inference is so last century. The right thing to do is to write the types down, and then get as much mechanical assistance generating the programs as possible."
— @pigworker
-
Show this thread
-
Actually I want both. Especially when making changes, sometimes I know what changes I want in the spec/type/prop and I want the compiler to help me with the impl/term/proof; other times vice versa.
1 reply 0 retweets 3 likes -
Fortunately, it's a trade off rather than an all-or-nothing choice. You can get a lot of inference even if you start with a top level type. I want both too!
1 reply 1 retweet 7 likes -
Replying to @edwinbrady @DaTwinkDaddy and
Presumably there's a type level debugger that assists me when my types are wrong ...
2 replies 0 retweets 9 likes -
Replying to @deech @edwinbrady and
Isn't this just a proof assistant really?
1 reply 0 retweets 2 likes
Replying to @mundoplano @deech and
It's pretty much what proof assistants do, but they're aimed at a different kind of user.
4:21 PM - 20 May 2019
0 replies
0 retweets
4 likes
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.