On May 12, 2017, at 6:46 AM, Anthony Clayden wrote:

So please explain here in what way type families are "half baked".

My interpretation of mniip’s use of this descriptor was a reference to the fact that type families aren’t just functions, don’t support `case`, can’t be partially applied, etc. Instead, we should just be able to use functions in types. :) I agree that closed type families are bizarre and perhaps a misfeature -- though I think they are a good incremental step toward something better. What would be far better is if we could just use `case`, and then the closed type family syntax would desugar into case statements, much like how normal functions work. So type family F a b where F Int b = b F a Bool = a (AntC’s example) would really mean type F a b = case a of Int -> b _ -> case b of Bool -> a _ -> F a b We understand the semantics of case expressions, so this would avoid the bizarreness of closed type families. (We would also have to eliminate non-linear patterns, replacing them with some other first-class test for equality. It’s currently unclear to me how to do this right. Section 5.13.2 of my thesis dwells on this, without much in the way of a concrete way forward.) AntC’s proposed disequality constraints then become straightforward pattern guards. Richard