Nick and I have a new draft out, on adding types for term-level equations to System F. Contrary to the experience of dependent types, this is not a very hairy extension -- in fact, I would not even hesitate to call it simple.
However, it does open the door to all sorts of exciting things, such as many peoples' long-standing goal of putting semantic properties of modules into the module interfaces. This is good for documentation, and also (I would hope) good for compilers --- imagine Haskell, if the Monad typeclass definition also told you (and ghc!) all the equational rewriting that it was supposed to do.
However, it does open the door to all sorts of exciting things, such as many peoples' long-standing goal of putting semantic properties of modules into the module interfaces. This is good for documentation, and also (I would hope) good for compilers --- imagine Haskell, if the Monad typeclass definition also told you (and ghc!) all the equational rewriting that it was supposed to do.
This comment has been removed by the author.
ReplyDeleteThis comment has been removed by the author.
ReplyDeleteWill this hypothetical version of Haskell allow us to write machine-checkable proofs of e.g. monad laws for custom Monad instances in the language itself?
ReplyDeleteIn fact, quite the opposite -- the whole point of our design is to *not* compel the use of the language itself for proofs. If you try to combine the two, you get systems of dependent types. Unfortunately, getting dependent types to play nicely with data abstraction is kind of an open reseach problem.
ReplyDeleteSo our idea is to give a language that doesn't support proving internal to the language, but does (a) support data abstraction well, and (b) gives you a clean way of shipping proof obligations to proof assistants like Coq. (After all, Coq already exists and there's no reason not to use it!)
There's a typo in the first sentence of the first paragraph of your Introduction.
ReplyDeleteThanks for clarification.
ReplyDeleteKarl: that's a hilariously awful typo. :(
ReplyDelete