and unless you have some way of classifying programs that are "relevant" to you and guaranteeing that your language can express those, that's a pretty massive restriction!
hmm i'm not sure about that! being turing incomplete can be useful (although that's usually more of a proxy factor, e.g. even in dhall you can still write programs that take 1000 years to complete) but it also means that there are programs that you just *cannot* write
like, have you ever tried to implement QuickSort in Coq? ^^
okay but can you implement all of your desired programs? even if you can, there is an additional burden to proving that e.g. interesting programs terminate that you just don't need without it. so it's not strictly better, is it?
Blazingly Fast Type Class Resolution with Tries
Haskell's tuples should behave like multi-element newtypes
Hear me out, I swear the title makes sense! What I mean is that tuples should have the same laziness characteristics as newtypes, just extended to more than one element. I'll explain what this means ...
I love how many facets of Haskell are embodied by the module Control.Monad.Trans
Type families are so nice and so horrible at the same time
A Monad Instance for Set: You didn't think I would give up that easily, did you?
The reason why Haskell's standard Set [https://hackage.haskell.org/package/containers-0.7/docs/Data-Set.html#t:Set] type doesn't implement Monad - and therefore cannot be used in monad comprehensions ...