Now that the Type Equality coercions extension is stable and has been blessed by SPJ as "a functional-dependency-like mechanism (but using equalities) for the result type" [in http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Hig herranktypesandtypefunctions], no code is compelled to use FunDeps. [Note that this is orthogonal to the issue of overlaps. You can use the equalities mechanism happily with overlaps, see example below. This is also orthogonal to type functions/families/associated types. You can use the equalities mechanism happily without type families.] There's plenty of code using FunDeps, so we couldn't just withdraw the extension. But we could start deprecating it. Better still, given that there is a mechanical way to convert FunDeps to equalities, we could start treating the FunDep on a class declaration as documentation, and validate that the instances observe the mechanical translation. Here's an example of the mechanical translation for HDeleteMany, the classic awkward example from HList. The problem is to delete all occurences of element type e in a HList l. Here's the 'non-solution' naieve attempt from the HList paper: class HDeleteMany e l l' | e l -> l' instance HDeleteMany a HNil HNil -- base case OK instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e l) l' -- element match, so omit instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e' l) (HCons e' l') -- element not match, so retain -- + recurse on the tail "The two overlapping instance heads for HCons are in no substitution ordering." Here's the mechanical translation, which _does_ compile: class HDeleteMany e l l' -- | e l -> l' instance (HNil ~ l') -- force the result => HDeleteMany a HNil l' -- base case OK instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e l) l' -- same as above instance (HList l, HDeleteMany e l l'', (HCons e' l'') ~ l') => HDeleteMany e (HCons e' l) l' -- force the result The translation rules (applying for the 'target' term of a FunDep) are: 1. If the target is a bare typevar not appearing otherwise in the head, we're done OK. Otherwise: 2. Replace the target with a fresh typevar. (This forces instance match without inspecting the use site.) 3. Add a type equality constraint equating the fresh typevar with the as-was target term. (This forces the result type, in the same way as a FunDep target.) Possible GSOC project?
1. What do you mean by deprecating? Deprecate it in GHC? What does it have to do with Haskell'? 2. What do you gain by doing so? 3. How do you translate cyclic dependencies? Roman * AntC <anthony_clayden@clear.net.nz> [2013-04-30 05:31:09+0000]
Now that the Type Equality coercions extension is stable and has been blessed by SPJ as "a functional-dependency-like mechanism (but using equalities) for the result type" [in http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Hig herranktypesandtypefunctions], no code is compelled to use FunDeps.
[Note that this is orthogonal to the issue of overlaps. You can use the equalities mechanism happily with overlaps, see example below. This is also orthogonal to type functions/families/associated types. You can use the equalities mechanism happily without type families.]
There's plenty of code using FunDeps, so we couldn't just withdraw the extension. But we could start deprecating it.
Better still, given that there is a mechanical way to convert FunDeps to equalities, we could start treating the FunDep on a class declaration as documentation, and validate that the instances observe the mechanical translation.
Here's an example of the mechanical translation for HDeleteMany, the classic awkward example from HList.
The problem is to delete all occurences of element type e in a HList l. Here's the 'non-solution' naieve attempt from the HList paper:
class HDeleteMany e l l' | e l -> l' instance HDeleteMany a HNil HNil -- base case OK instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e l) l' -- element match, so omit instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e' l) (HCons e' l') -- element not match, so retain -- + recurse on the tail
"The two overlapping instance heads for HCons are in no substitution ordering."
Here's the mechanical translation, which _does_ compile:
class HDeleteMany e l l' -- | e l -> l' instance (HNil ~ l') -- force the result => HDeleteMany a HNil l' -- base case OK instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e l) l' -- same as above instance (HList l, HDeleteMany e l l'', (HCons e' l'') ~ l') => HDeleteMany e (HCons e' l) l' -- force the result
The translation rules (applying for the 'target' term of a FunDep) are: 1. If the target is a bare typevar not appearing otherwise in the head, we're done OK. Otherwise: 2. Replace the target with a fresh typevar. (This forces instance match without inspecting the use site.) 3. Add a type equality constraint equating the fresh typevar with the as-was target term. (This forces the result type, in the same way as a FunDep target.)
Possible GSOC project?
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Roman Cheplyaka <roma@...> writes:
1. What do you mean by deprecating? Deprecate it in GHC? What does it have to do with Haskell'? 2. What do you gain by doing so?
GHC is the de facto testing ground for ideas 'on the menu' for Haskell'. H' has been in paralysis for years around MPTC, Overlaps, FunDeps/Type Families (functions). I'm trying to see a way to remove one of the options so that we can simplify the choices/move the logjam. So yes, I mean deprecate in GHC.
3. How do you translate cyclic dependencies?
You can get an equivalent to cyclic dependencies using equality constraints. (I'll reply to Oleg's example of Sum.) But I agree that my mechanical translation doesn't usually get you to the result. So my GSOC project idea would be to see how far you might get with a more sophisticated translation. Anthony
You can get an equivalent to cyclic dependencies using equality constraints. (I'll reply to Oleg's example of Sum.) But I agree that my mechanical translation doesn't usually get you to the result.
So my GSOC project idea would be to see how far you might get with a more sophisticated translation.
Just assuming for the moment that you can actually translate fundeps completely into type equality coercions. Then that would be, to me, a good reason to (A) make sure that the implementation actually uses this encoding internally, and (B) keep fundep notation as syntactic sugar. I think the main "problem" of the type families vs. fundeps discussion is that they're two rather involved language extensions that in addition have very subtle differences. In this situation, you wouldn't really want to have both be an official part of the language (although that's the de facto reality we're living in since many years). If, however, there's a correct and complete unification of the two concepts in terms of a common underlying formalism, then I don't necessarily see why we should deprecate one. Cheers, Andres
Andres Löh <andres.loeh@...> writes: ...
I think the main "problem" of the type families vs. fundeps discussion is that they're two rather involved language extensions that in addition have very subtle differences.
Thanks Andres, but let me be clear: I am _not_ discussing Type Families vs. FunDeps. I'm talking about equality constraints only. Yes, equalities and Type Families arrived (in GHC) at the same time, but they are different features. (There were many creative ways to achieve something like equality constraints long before the TF work. For example various TypeCast's in the HList work. And really the compiler's type inference is just equality constraint-solving. What arrived in GHC was making equalities explicit in the surface language, and making sure it integrated with type inference.) There are some not-so-subtle differences between TF's and FunDeps. Especially that FunDeps support overlaps (well, up to a point) -- so no surprise that the counter-examples in Oleg's post concentrate on overlap problems. I am certainly not suggesting that equalities 'solve' those problems. I am saying they're no worse than FunDeps. And that by taking away FunDeps we simplify the choices around MPTC's in Haskell Prime.
... If, however, there's a correct and complete unification of the two concepts in terms of a common underlying formalism,
If by "the two concepts" you mean TF's and FunDeps, then: no, there is no such unification. (There are many commonalities, but as you say, subtle/frustrating differences.) I am claiming FunDeps can be expressed as equality constraints. I'm also of the opinion that FunDeps require a mental model that doesn't fit well with a functional language. So I'm arguing for simplification.
It seems to be my day to be the villain crying out against everything someone proposes. ;) I for one would be strongly against a proposal that started actively deprecating the use of functional dependencies in user code. There are a number of situations where the sheer amount of code you're forced to write by the mechanical translation to equalities and type families is explosive. I have dozens of classes of forms like class Wrapped s t a b | a -> s, b -> t, a t -> s, b s -> t that become frankly nigh unusable after translation -- other examples are much worse. Similarly, in my experience, code written with monads-tf is almost always about 15% more verbose than code written with the mtl. It costs me two characters to put a space and an 's' in for MonadState s m, but I'm usually not talking about the class unless I also reference the state type in the signature later, and there it saves me several characters per occurrence. When you have a more complicated functional dependency set like the above, though the difference isn't just a small constant amount of overhead. It isn't that I use these things out of ignorance. I use them deliberately when the alternative isn't palatable. I'm all for internally desugaring everything into the same form internally, but Haskell as a culture has long embraced surface complexity so long as it can desugar to something internally reasonable: Consider, let vs. where, multiple definitions vs. case, layout vs. {}'s, etc. This is despite their varying surface complexities. Let is an expression and where being tied to the binding over statements, multiple bindings permitting you to shuffle backtrack pattern matches and guards across several arguments, etc. Even changing out the implementation strategy for FDs in GHC has not been without pain, as it has resulted in changing the semantics of a number of corner cases. In fact, one could argue a large part of the stall in there being any progress in standardizing something in the TF vs FD vs both arena has been that it is very much a moving target. The document we would write today bears very little resemblance to the document we'd have written 5 years ago. To standardize something you need to know what it means. If we'd standardized FDs 5 years ago, we'd be sitting here with an increasingly irrelevant language standard today or stuck in our tracks, and with very little practical impact on the community to show for it, and we'd be likely rewriting the whole document now. It takes a lot of effort to write up something like either TFs or FDs in their full generality, and the resulting document if based on just transcoding the state of GHC documents an implementation, not necessarily the most reasonable commonly agreeable semantics. Arguably haskell-prime's role should be to follow far enough behind that the right decisions can be reached by implementations that blaze ahead of it. The only Haskell compiler even with type equalities is GHC at this point. They aren't a small change to introduce to a compiler. I for one work on a rather Haskelly compiler for my day job, when I'm not crying gloom and doom on mailing lists, and have been actively considering how to go about it for almost two years now without losing the other properties that make that compiler special. I'd really be a lot more comfortable having seen more success stories of people converting Haskell compilers over to this kind of approach before I felt it wise to say that this way that we know works and which has been productively in use in real code for ten years should be deprecated in favor of a way that only works with the single compiler. A large part of the pain of "choosing between" FDs and TFs is that both have different somewhat overlapping strengths. In the end I don't think we will wind up choosing between them, we'll just desugar both to a common core. Hopefully after we have more than one point in the design space to choose from. Removing a language feature just because another one can duplicate it with explosively more verbose code doesn't strike me as a very Haskelly way forward. -Edward On Tue, Apr 30, 2013 at 1:31 AM, AntC <anthony_clayden@clear.net.nz> wrote:
Now that the Type Equality coercions extension is stable and has been blessed by SPJ as "a functional-dependency-like mechanism (but using equalities) for the result type" [in http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Hig herranktypesandtypefunctions], no code is compelled to use FunDeps.
[Note that this is orthogonal to the issue of overlaps. You can use the equalities mechanism happily with overlaps, see example below. This is also orthogonal to type functions/families/associated types. You can use the equalities mechanism happily without type families.]
There's plenty of code using FunDeps, so we couldn't just withdraw the extension. But we could start deprecating it.
Better still, given that there is a mechanical way to convert FunDeps to equalities, we could start treating the FunDep on a class declaration as documentation, and validate that the instances observe the mechanical translation.
Here's an example of the mechanical translation for HDeleteMany, the classic awkward example from HList.
The problem is to delete all occurences of element type e in a HList l. Here's the 'non-solution' naieve attempt from the HList paper:
class HDeleteMany e l l' | e l -> l' instance HDeleteMany a HNil HNil -- base case OK instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e l) l' -- element match, so omit instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e' l) (HCons e' l') -- element not match, so retain -- + recurse on the tail
"The two overlapping instance heads for HCons are in no substitution ordering."
Here's the mechanical translation, which _does_ compile:
class HDeleteMany e l l' -- | e l -> l' instance (HNil ~ l') -- force the result => HDeleteMany a HNil l' -- base case OK instance (HList l, HDeleteMany e l l') => HDeleteMany e (HCons e l) l' -- same as above instance (HList l, HDeleteMany e l l'', (HCons e' l'') ~ l') => HDeleteMany e (HCons e' l) l' -- force the result
The translation rules (applying for the 'target' term of a FunDep) are: 1. If the target is a bare typevar not appearing otherwise in the head, we're done OK. Otherwise: 2. Replace the target with a fresh typevar. (This forces instance match without inspecting the use site.) 3. Add a type equality constraint equating the fresh typevar with the as-was target term. (This forces the result type, in the same way as a FunDep target.)
Possible GSOC project?
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Er, what I meant was class Foo s t a b | s -> a, t -> b, s b -> t, t a -> s That is what I get for dashing it off off the cuff. =) Then s determines some type argument for it, t determines its type argument, but Using s and the other type argument I can determine the whole containing type 't' and vice versa. instance Foo (Identity a) (Identity b) a b On Wed, May 1, 2013 at 7:02 AM, Ian Lynagh <ian@well-typed.com> wrote:
On Tue, Apr 30, 2013 at 11:35:10PM -0400, Edward Kmett wrote:
I have dozens of classes of forms like
class Wrapped s t a b | a -> s, b -> t, a t -> s, b s -> t
Isn't this equivalent to just
class Wrapped s t a b | a -> s, b -> t
?
Thanks Ian
participants (5)
-
Andres Löh -
AntC -
Edward Kmett -
Ian Lynagh -
Roman Cheplyaka