Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
2 days ago Richard Eisenberg (and mniip) wrote:
... On incremental improvements / the "half-baked" nature of type families: I agree completely. ... ["half-baked" is Richard quoting mniip]
... the weird place of type families in the language. It is my hope that Dependent Haskell will obviate a lot of these concerns, allowing us to deprecate type families as we know them (you would just use an ordinary function in types instead).
I don't want to sidetrack the github discussion on mniip's proposal. https://github.com/ghc-proposals/ghc-proposals/pull/52 So please explain here in what way type families are "half baked". The part of type families I find hard to use and hard to reason about is closed type families. I'd be very happy to deprecate them, if there was something that did overlaps better.
From what I can make out, though, in Richard's Dissertation, they can't be promoted to "ordinary functions in types".
If the closed equations were ordinary functions in types, you could go:
type family F a b type instance F Int b = b type instance F a Bool | a /~ Int = a -- non-unifiability guard
With no need for a closed sequence of choices. Is this the "case-like computations" others talk about on the proposal? AntC
On May 12, 2017, at 6:46 AM, Anthony Clayden <anthony_clayden@clear.net.nz> 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
On Fri, May 12, 2017 at 01:22:35PM -0400, Richard Eisenberg wrote:
On May 12, 2017, at 6:46 AM, Anthony Clayden <anthony_clayden@clear.net.nz> 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. :)
That is very much correct, but what I was exactly referring to was not the necessary limitations of type families (such as inability of partial application) but rather their unnecessary limitations. For example only being able to pattern-match at the top-level, or, with InjectiveTypeFamilies, lack of 'result arg1 -> arg2' type injectivity.
I agree that closed type families are bizarre and perhaps a misfeature -- though I think they are a good incremental step toward something better.
Closed type families have proven very useful to me, so I don't agree with calling them a misfeature, however I can see where you're coming from : throughout the entire language we enforce the notion that we can't have a "proof of type inequality" and then closed type families give us just that. Indeed, their semantics could be made more apparent.
participants (3)
-
Anthony Clayden -
mniip -
Richard Eisenberg