Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
What's the expressiveness of GADTs? Or conversely, what inductive types (that would be expressible in Coq or any fancier dependently typed language for example) are not expressible with GADTs?
Well formed inductive types? :wink:
Are you referring to the way types in Haskell are full of weird inhabitants?
Apparently the only difference other than that is the lack of type-level lambdas.
I was being cheeky -- I'm far from an expert but yes, inhabitants. And I'm not sure on this one but can Haskell express universes?
I don't think so, but thanks for mentioning it since I hadn't thought about it :)
Theres http://hackage.haskell.org/package/universe, though I haven't dug into it enough to know how it works
What's the expressiveness of GADTs? Or conversely, what inductive types (that would be expressible in Coq or any fancier dependently typed language for example) are not expressible with GADTs?
Well formed inductive types? :wink:
Are you referring to the way types in Haskell are full of weird inhabitants?
Apparently the only difference other than that is the lack of type-level lambdas.
I was being cheeky -- I'm far from an expert but yes, inhabitants. And I'm not sure on this one but can Haskell express universes?
I don't think so, but thanks for mentioning it since I hadn't thought about it :)
Theres http://hackage.haskell.org/package/universe, though I haven't dug into it enough to know how it works