TypeFamilies vs. FunctionalDependencies & type-level recursion
Dan Doel wrote: >class C a b | a -> b where > foo :: a -> b > foo = error "Yo dawg." > >instance C a b where The instance 'C a b' blatantly violates functional dependency and should not have been accepted. The fact that it was is a known bug in GHC. The bug keeps getting mentioned on Haskell mailing lists about every year. Alas, it is still not fixed. Here is one of the earlier messages about it: http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html HList does NOT depend on that invalid behavior. The bug is relatively recent (introduced around 2006); HList worked in 2004. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
I'd like to summarize the relationship between functional dependencies and type functions, and propose a solution that should get rid of overlapping instances. The solution does not require messing with System-FC. In fact, it can be implemented today (although ungainly). A small bit of GHC support will be appreciated. I believe that functional dependencies and type functions are not comparable. There are examples that can't be done (in principle or in practice) with type functions, and there are examples that cannot be implemented with functional dependencies. The example of the latter is http://okmij.org/ftp/Computation/extra-polymorphism.html#injectivity Functional dependencies have the advantage in the following two cases 1. mutual dependencies: class Add x y z | x y -> z, x z -> y, y z -> x I think this example can be emulated with type functions; the emulation didn't work with GHC 6.10, at least. It may work now. 2. combination with overlapping instances The type equality predicate is only one example, there are several of that kind. Just for the record, the following code class Eq a b c | a b -> c instance Eq k k True instance Eq j k False never worked. (GHC may have accepted the above declarations; that doesn't mean much since overlapping was detected lazily). The key insight of HList is the realization why the code above did not work and how to hack around it (TypeCast or ~ is needed). If GHC somehow provided Eq as a built-in, that would not have been enough. We need something like Eq at higher kinds. For example, http://okmij.org/ftp/Haskell/typecast.html#is-function-type That web page gives example of IsList, IsArray and other such predicates. The most practical application of overlapping instances is documented in http://www.haskell.org/pipermail/haskell-cafe/2010-June/078590.html http://www.haskell.org/pipermail/haskell-cafe/2010-June/078739.html The solution has been described already in the HList paper: provide something the typeOf at the type level. That is, assume a type function TypeOf :: * -> TYPEREP where TYPEREP is a family of types that describe the type of TypeOf's argument in the way TypeRep value described the type. The HList paper (Sec 9) has outlined an ugly solution: associate with each type constructor a type-level numeral; TYPEREP is a type-level list then, which contains the code for the head constructor and TYPEREPs of the arguments. TYPEREPs are easily comparable. The HList solution is certainly ugly and non-scalable. The biggest problem is assigning opaque integers to type constructors and ensuring the uniqueness. Once I toyed with the idea of defining a family of types to be the HList of Dot and Dash, so we would spell the name of the constructor in Morse code. I must stress that my proposal is rather timid: Matthias Blume, when designing a new FFI for SML/NJ has lifted the whole latin alphabet to the type level: http://people.cs.uchicago.edu/~blume/papers/nlffi-entcs.pdf so he could spell the names of C struct in SML types. This NLFFI has been used in SML/NJ, in production, for about 10 years. If SML developers could do that, certainly GHC developers could. Persistent rumors hold that someone is working on adding more kinds to GHC. A Kind NAME and a Kind TYPEREP seem good kinds to have (along with naturals, of course). GHC could then provide the type function TypeOf. Once we have a TYPEREP, we can compare and deconstruct it, removing the need for overlapping instances. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
At Tue, 14 Jun 2011 19:21:38 -0400, Dan Doel wrote: > > If this is really about rules for selecting instances unambiguously > without any regard to whether some parameters are actually functions > of other parameters, then the name "functional dependencies" is pretty > poor. Maybe "functional dependencies" is a poor name. I'm not going to argue it's a good one, just that the extension is quite useful. Despite what the name suggests, it is most useful to think of "| a b -> c d" as meaning "any method that uses types a and b does not need to use types c and d for the compiler to determine a unique instance". Once you start thinking of fundeps that way (and always keep in mind that contexts play no role in instance selection), then I think it gets a bit easier to reason about fundeps. > I know the actual implementation is, too. But it's because of the > limited way in which fundeps are used. If I'm not mistaken, if they > were modified to interact with local constraints more like type > families (that is, correctly :)), then soundness would be a concern > with these examples. I don't think so. Because fundeps (despite the name) are mostly about instance selection, incoherent fundeps won't violate safety. Your program may incoherently chose between methods in multiple instances that should be the same instance, but at least each individual method is type safe. With type families, you can actually undermine type safety, and there's no cheating way to fix this, which is why I think TypeFamilies could by very dangerous when combined with dynamic loading. > I understand why the instance resolution causes these to be different > in Haskell. I think the first one is a bad definition by the same > criteria (although it is in practice correct due to the constraint), > but UndecidableInstances turns off the check that would invalidate it. Though I realize you are unlikely ever to like lifting the coverage condition, let me at least leave you with a better example of why Undecidable instances are useful. Suppose you want to define an instance of MonadState for another monad like MaybeT. You would need to write code like this: instance (MonadState s m) => MonadState s (MaybeT m) where get = lift get put = lift . put This code fails the coverage condition, because class argument (MaybeT m) does not contain the type variable s. Yet, unlike the compiler, we humans can look at the type context when reasoning about instance selection. We know that even though our get method is returning an s--meaning really "forall s. s", since s is mentioned nowhere else--there is really only one s that will satisfy the MonadState s m requirement in the context. Perhaps more importantly, we know that in any event, if the code compiles, the s we get is the one that the surrounding code (calling get or put) expects. Now if, in addition to lifting the coverage condition, you add OverlappingInstances, you can do something even better--you can write one single recursive definition of MonadState that works for all MonadTrans types (along with a base case for StateT). This is far preferable to the N^2 boilerplate functions currently required by N monad transformers: instance (Monad m) => MonadState s (StateT s m) where get = StateT $ \s -> return (s, s) instance (Monad (t m), MonadTrans t, MonadState s m) => MonadState s (t m) where get = lift get put = lift . put This is not something you can do with type families. So while UndecidableInstances and OverlappingInstances aren't very elegant, the fact that they can reduce source code size from O(N^2) to O(N) is a good indication that there is some unmet need in the base language. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
On Tue, Jun 14, 2011 at 5:38 PM,
wrote:
> Undecidable instances are orthogonal to both FunctionalDependencies
> and OverlappingInstances. They concern whether or not the compiler
> can guarantee that the typechecker will terminate. You can have
> undecidable instances without either of the other two extensions
I'm aware of what UndecidableInstances does.
But in this case, it's actually ensuring the soundness of the
computational aspect of functional dependencies, at least in the case
where said computation were fixed to incorporate the things type
families can do. Which would be useful, because fundeps don't interact
with GADTs and such correctly.
> The coverage condition is part of a pair of pair of sufficient (but
> not necessary) conditions that GHC applies to know that typechecking
> is decidable. It just says that if you have a dependency "a -> b",
> and you have type variables in b, then they should mention all the
> type variables in a. Thus, the following code is legal without
> UndecidableInstances:
>
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE FunctionalDependencies #-}
>
> class A a b | a -> b
> instance A [a] (Either String a)
In this instance, the second argument can be given as a function of the first:
f [a] = Either String a
> But the following program is not:
>
> class A a b | a -> b
> instance A a (Either String b)
In this instance, it cannot.
> No, that's not right. Even with UndecidableInstances, you cannot
> define conflicting instances for functional dependencies. Moreover,
> just because the GHC's particular typechecker heuristics don't
> guarantee the above code is decidable doesn't mean it isn't decidable.
You certainly can define conflicting instances if 'a -> b' is supposed
to denote a functional dependency between a and b, and not just a
clever set of rules for selecting instances.
> I think you are thinking of UndecidableInstances in the wrong way.
> For instance, the following code does not require
> UndecidableInstances, but has polymorphic type variables on the
> right-hand side of a functional dependency, which seems to be what you
> object to:
>
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FunctionalDependencies #-}
>
> class C a b | a -> b where
> foo :: a -> b
>
> instance C (Either a b) (Maybe b) where
> foo _ = Nothing
>
> bar :: Maybe Int
> bar = foo (Left "x")
>
> baz :: Maybe Char
> baz = foo (Left "x")
This is another case where the second argument is a function of the first:
f (Either a b) = Maybe b
bar uses the induced instance C (Either String Int) (Maybe Int), and
baz uses the induced instance C (Either String Char) (Maybe Char).
> Remember, FunctionalDependencies are all about determining which
> instance you select. The functional dependency "class C a b | a -> b"
> says that for a given type a, you can decide which instance of C
> (i.e., which particular function foo) to invoke without regard to the
> type b.
Why are they called "functional dependencies" with "a -> b" presumably
being read "b functionally depends on a" if there is no actual
requirement for b to be a function of a?
> It specifically does *not* say whether or not type b has to
> be grounded, or whether it may include free type variables, including
> just being a type variable if you enable FlexibleInstances:
I don't personally count free type metavariables as Haskell types.
They are artifacts of the inference algorithm. Int is a type, and
(forall a. a) is a type. But a metavariable 'b' is just standing in
for a type until we can figure out what actual Haskell type it should
be. Haskell muddies this distinction by only allowing prenex
quantification, and writing 'a -> b' instead of 'forall a b. a -> b',
but the distinction is actually important, if you ask me.
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FunctionalDependencies #-}
> {-# LANGUAGE FlexibleInstances #-}
>
> class C a b | a -> b where
> foo :: a -> b
>
> instance C (Either a b) b where -- no UndecidableInstances needed
> foo _ = undefined
This is yet another example where the second parameter is actually a
function of the first.
> Again, unique but not grounded. Either Maybe c or "forall c" is a
> perfectly valid unique type, though it's not grounded. People do
> weird type-level computations with fundeps using types that aren't
> forall c. (The compiler will fail if you additionally have an
> instance with forall c.)
(forall c. Either Maybe c) is a valid type. "forall c" on its own is
not a type at all, it's a syntax error. And a metavariable 'c' is
something that exists during inference but not in the type system
proper.
> I think the reason you have the right-hand side is so you can
> say things like "| a -> b, b -> a".
The reason they h
RE: TypeFamilies vs. FunctionalDependencies & type-level recursion
Some brief rejoinders.
1. Golly, functional dependencies are tricky aren't they? A big reason I like
type families better is simply that I can understand them.
2. Thank you for correcting my equality example. The code I gave
>class Eq a b c | a b -> c
>instance Eq k k True
>instance Eq j k False
doesn't work, and has never worked. The form that does work is
>class Eq a b c | a b -> c
>instance Eq k k True
>instance (r~False) => Eq j k r
3. There have been some questions about soundness and fundeps. Don't worry.
I'm certain GHC's implementation fundeps is sound. Fundeps in GHC are used
*only* to add extra equality constraints that do some extra unifications. (Yes
this is a statement about the type inference algorithm, rather than about the
type system. I don't know how to give a satisfactory non-algorithmic
treatment of fundeps.)
GHC then translates the type-checked program into System FC, and (if you use
-dcore-lint) is redundantly typechecked there (no fundeps involved). So, no
soundness worries: GHC may reject a program you want it to accept, but a
program it accepts won't go wrong at runtime. [Barring the notorious Trac
#1496]
4. Dan asks why
instance (r~False) => Eq j k r
could possibly differ from
instance Eq j k False
The reason is this. You could imagine permitting this:
instance C a => C [a]
instance D a => C [a]
meaning "to satisfy C [a] try to satisfy C a. Failing that, you can instead try
D a". So constraint solving would need a search process. But Haskell doesn't
do that. It insists that instance "heads", C [a] in this case, are distinct.
(Usually non-overlapping.) So the instance head (Eq j k r) is different from
(Eq j k False); the latter matches more often, but then requires (r~False).
Simon
| -Original Message-
| From: haskell-prime-boun...@haskell.org [mailto:haskell-prime-
| boun...@haskell.org] On Behalf Of dm-list-haskell-pr...@scs.stanford.edu
| Sent: 14 June 2011 22:39
| To: Dan Doel
| Cc: haskell-prime@haskell.org
| Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
|
| At Tue, 14 Jun 2011 15:09:02 -0400,
| Dan Doel wrote:
| >
| > On Tue, Jun 14, 2011 at 1:19 PM,
| > wrote:
| > > No, these are not equivalent. The first one "TypeEq a b c" is just
| > > declaring an instance that works "forall c". The second is declaring
| > > multiple instances, which, if there were class methods, could have
| > > different code. The second one is illegal, because given just the
| > > first two types, a and b, you cannot tell which instance to pick.
| >
| > Then why am I not allowed to write:
| >
| > class C a b | a -> b
| > instance C T [a]
| >
| > without undecidable instances? GHC actually complains in that case
| > that the coverage condition is violated. But it is a single well
| > specified instance that works for all a.
|
| Undecidable instances are orthogonal to both FunctionalDependencies
| and OverlappingInstances. They concern whether or not the compiler
| can guarantee that the typechecker will terminate. You can have
| undecidable instances without either of the other two extensions, for
| instance:
|
| {-# LANGUAGE FlexibleInstances #-}
|
| class A a
| class B a
| instance (A a) => B a -- illegal w/o UndecidableInstances
|
| The coverage condition is part of a pair of pair of sufficient (but
| not necessary) conditions that GHC applies to know that typechecking
| is decidable. It just says that if you have a dependency "a -> b",
| and you have type variables in b, then they should mention all the
| type variables in a. Thus, the following code is legal without
| UndecidableInstances:
|
| {-# LANGUAGE MultiParamTypeClasses #-}
| {-# LANGUAGE FlexibleInstances #-}
| {-# LANGUAGE FunctionalDependencies #-}
|
| class A a b | a -> b
| instance A [a] (Either String a)
|
| But the following program is not:
|
| class A a b | a -> b
| instance A a (Either String b)
|
| > The answer is that such an instance actually violates the functional
| > dependency, but UndecidableInstances just turns off the checks to make
| > sure that fundeps are actually functional. It's a, "trust me," switch
| > in this case (not just a, "my types might loop," switch).
|
| No, that's not right. Even with UndecidableInstances, you cannot
| define conflicting instances for functional dependencies. Moreover,
| just because the GHC's particular typechecker heuristics don't
| guarantee the above code is decidable doesn't mean it isn't decidable.
|
| > So I guess HList will still work fine, and UndecidableInstances are
| > actually more evil than I'd previously thought (thanks for the
| > correction, Andrea :)).
|
| I think you are thinking of UndecidableInstances in the wrong way.
| For instance, the following
RE: TypeFamilies vs. FunctionalDependencies & type-level recursion
| http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies | | Currently under cons for FunctionalDependencies, it says: | | AssociatedTypes seem to be more promising. | | I proposed the following fix: | | AssociatedTypes seem to be more promising, but in their | current form are not as general as FunctionalDependencies | [link]. OK, that one. I've made that change. | Is there a policy that only a proposal's "owner" can modify the wiki | page? Or that you have to be a member of the Haskell' committee? I'm not sure. Malcolm Wallace is chair at the moment; I'm ccing him. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
At Tue, 14 Jun 2011 15:09:02 -0400,
Dan Doel wrote:
>
> On Tue, Jun 14, 2011 at 1:19 PM,
> wrote:
> > No, these are not equivalent. The first one "TypeEq a b c" is just
> > declaring an instance that works "forall c". The second is declaring
> > multiple instances, which, if there were class methods, could have
> > different code. The second one is illegal, because given just the
> > first two types, a and b, you cannot tell which instance to pick.
>
> Then why am I not allowed to write:
>
> class C a b | a -> b
> instance C T [a]
>
> without undecidable instances? GHC actually complains in that case
> that the coverage condition is violated. But it is a single well
> specified instance that works for all a.
Undecidable instances are orthogonal to both FunctionalDependencies
and OverlappingInstances. They concern whether or not the compiler
can guarantee that the typechecker will terminate. You can have
undecidable instances without either of the other two extensions, for
instance:
{-# LANGUAGE FlexibleInstances #-}
class A a
class B a
instance (A a) => B a -- illegal w/o UndecidableInstances
The coverage condition is part of a pair of pair of sufficient (but
not necessary) conditions that GHC applies to know that typechecking
is decidable. It just says that if you have a dependency "a -> b",
and you have type variables in b, then they should mention all the
type variables in a. Thus, the following code is legal without
UndecidableInstances:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
class A a b | a -> b
instance A [a] (Either String a)
But the following program is not:
class A a b | a -> b
instance A a (Either String b)
> The answer is that such an instance actually violates the functional
> dependency, but UndecidableInstances just turns off the checks to make
> sure that fundeps are actually functional. It's a, "trust me," switch
> in this case (not just a, "my types might loop," switch).
No, that's not right. Even with UndecidableInstances, you cannot
define conflicting instances for functional dependencies. Moreover,
just because the GHC's particular typechecker heuristics don't
guarantee the above code is decidable doesn't mean it isn't decidable.
> So I guess HList will still work fine, and UndecidableInstances are
> actually more evil than I'd previously thought (thanks for the
> correction, Andrea :)).
I think you are thinking of UndecidableInstances in the wrong way.
For instance, the following code does not require
UndecidableInstances, but has polymorphic type variables on the
right-hand side of a functional dependency, which seems to be what you
object to:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
class C a b | a -> b where
foo :: a -> b
instance C (Either a b) (Maybe b) where
foo _ = Nothing
bar :: Maybe Int
bar = foo (Left "x")
baz :: Maybe Char
baz = foo (Left "x")
Remember, FunctionalDependencies are all about determining which
instance you select. The functional dependency "class C a b | a -> b"
says that for a given type a, you can decide which instance of C
(i.e., which particular function foo) to invoke without regard to the
type b. It specifically does *not* say whether or not type b has to
be grounded, or whether it may include free type variables, including
just being a type variable if you enable FlexibleInstances:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
class C a b | a -> b where
foo :: a -> b
instance C (Either a b) b where -- no UndecidableInstances needed
foo _ = undefined
> > A functional dependency such as "| a b -> c d" just guarantees that a
> > and b uniquely determine the instance. Hence, it is okay to have
> > class methods that do not mention type variables c and d, because the
> > compiler will still know which instance to pick.
>
> It specifies that a and b uniquely determine c and d, so the choice of
> instances is unambiguous based only on a and b.
Yes, but it doesn't say the c and d are ground types. c can be
(Maybe c'), or, with flexible instances it can just be some free type
variable c''.
> This is the basis for type level computation that people do with
> fundeps, because a fundep 'a b -> c' allows one to compute a unique
> c for each pair of types.
Again, unique but not grounded. Either Maybe c or "forall c" is a
perfectly valid unique type, though it's not grounded. People do
weird type-level computations with fundeps using types that aren't
forall c. (The compiler will fail if you additionally have an
instance with forall c.)
> Being allowed to elide variables from the types of methods
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
On Tue, Jun 14, 2011 at 1:19 PM, wrote: > No, these are not equivalent. The first one "TypeEq a b c" is just > declaring an instance that works "forall c". The second is declaring > multiple instances, which, if there were class methods, could have > different code. The second one is illegal, because given just the > first two types, a and b, you cannot tell which instance to pick. Then why am I not allowed to write: class C a b | a -> b instance C T [a] without undecidable instances? GHC actually complains in that case that the coverage condition is violated. But it is a single well specified instance that works for all a. The answer is that such an instance actually violates the functional dependency, but UndecidableInstances just turns off the checks to make sure that fundeps are actually functional. It's a, "trust me," switch in this case (not just a, "my types might loop," switch). So I guess HList will still work fine, and UndecidableInstances are actually more evil than I'd previously thought (thanks for the correction, Andrea :)). > A functional dependency such as "| a b -> c d" just guarantees that a > and b uniquely determine the instance. Hence, it is okay to have > class methods that do not mention type variables c and d, because the > compiler will still know which instance to pick. It specifies that a and b uniquely determine c and d, so the choice of instances is unambiguous based only on a and b. This is the basis for type level computation that people do with fundeps, because a fundep 'a b -> c' allows one to compute a unique c for each pair of types. If it were just about variable sets determining the instance, then we could just list those. But I can write: class C a b c d | a b -> c And it will actually be a, b and d that determine the particular instance, but just listing 'a b d', or using the fundep 'a b d -> c' is wrong, because the fundep above specifies that there is a single choice of c for each a and b. So we could have: C Int Int Char Int C Int Int Char Double C Int Int Char Float but trying to add: C Int Int Int Char to the first three would be an error, because the first two parameters determine the third, rather than the first, second and fourth. Being allowed to elide variables from the types of methods is one of the uses of fundeps, and probably why they were introduced, but it is not what fundeps mean. > On the other hand, though the compiler won't accept it, you could at > least theoretically allow code such as the following: > > instance C [Char] where > type Foo [Char] = forall b. () => b The fundep equivalent of this is not 'instance C [Char] b'. It is: instance C [Char] (forall b. b) except types like that aren't allowed in instances (for good reason in general). The closest you could come to 'instance C T b' would be something like: type instance F T = b except that is probably interpreted by GHC as being (forall b. b). -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
At Tue, 14 Jun 2011 12:31:47 -0400, Dan Doel wrote: > > Sorry about the double send, David. I forgot to switch to reply-all in > the gmail interface. > > Okay. I don't really write a lot of code like this, so maybe I missed > the quirks. > > In that case, HList has been relying on broken behavior of fundeps for > 7 years. :) Because the instance: > > instance TypeEq a b c > > violates the functional dependency, by declaring: > > instance TypeEq Int Int Int > instance TypeEq Int Int Char > instance TypeEq Int Int Double No, these are not equivalent. The first one "TypeEq a b c" is just declaring an instance that works "forall c". The second is declaring multiple instances, which, if there were class methods, could have different code. The second one is illegal, because given just the first two types, a and b, you cannot tell which instance to pick. > class C a b | a -> b where > foo :: a -> b > foo = error "Yo dawg." > > instance C a b where > > bar :: Int > bar = foo "x" > > baz :: Char > baz = foo "x" > > so we're using an instance C String Int and an instance C String Char > despite the fact that there's a functional dependency from the first > argument to the second. A functional dependency such as "| a b -> c d" just guarantees that a and b uniquely determine the instance. Hence, it is okay to have class methods that do not mention type variables c and d, because the compiler will still know which instance to pick. Since your code only has one instance of class C, the unique instance is trivially guaranteed and the code is fine. In fact, your code is effectively the same as: class C a where foo :: a -> b foo = error "Yo dawg." instance C a where The same issues happen with type families. The following code is obviously illegal, because you have a duplicate instance of class C: class C a where type Foo a foo :: a -> Foo a foo = error "Yo dawg." instance C [Char] where type Foo [Char] = Int instance C [Char] where type Foo [Char] = Char On the other hand, though the compiler won't accept it, you could at least theoretically allow code such as the following: instance C [Char] where type Foo [Char] = forall b. () => b David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
On Tue, Jun 14, 2011 at 6:31 PM, Dan Doel wrote:
> Sorry about the double send, David. I forgot to switch to reply-all in
> the gmail interface.
>
> On Tue, Jun 14, 2011 at 11:49 AM,
> wrote:
>> You absolutely still can use FunctionalDependencies to determine type
>> equality in GHC 7. For example, I just verified the code below with
>> GHC 7.02:
>>
>> *Main> typeEq True False
>> HTrue
>> *Main> typeEq (1 :: Int) (2 :: Int)
>> HTrue
>> *Main> typeEq (1 :: Int) False
>> HFalse
>>
>> As always, you have to make sure one of the overlapping instances is
>> more specific than the other, which you can do by substituting a
>> parameter c for HFalse in the false case and fixing c to HFalse using
>> another class like TypeCast in the context. (As contexts play no role
>> in instance selection, they don't make the instance any more
>> specific.)
>>
>> While I don't have convenient access to GHC 6 right this second, I'm
>> pretty sure there has been no change for a while, as the HList paper
>> discussed this topic in 2004.
>
> Okay. I don't really write a lot of code like this, so maybe I missed
> the quirks.
>
> In that case, HList has been relying on broken behavior of fundeps for
> 7 years. :) Because the instance:
>
> instance TypeEq a b c
>
> violates the functional dependency, by declaring:
>
> instance TypeEq Int Int Int
> instance TypeEq Int Int Char
> instance TypeEq Int Int Double
> ...
> instance TypeEq Int Char Int
> instance TypeEq Int Char Char
> ...
>
> and adding the constraint doesn't actually affect which instances are
> being declared, it just adds a constraint requirement for when any of
> the instances are used.
I think we can argue on the truth of this point, since i don't think
that e.g. instance Ord a => Ord [a] where {...} declares an instance
for Ord [Int -> Int], even if instance resolution won't look at the
context at first.
HList is ensuring the fundep is respected, which has to be done by the
programmer when one is using UndecidableInstances, by relying on the
fact that with OverlappingInstances a more general instance matches
only when a more specific one can be shown not to match (one problem
here is that this assumption is currently broken for type variables
that come out of an existential wrapper, but surprisingly not so for
the equivalent RankNTypes encoding).
-- Andrea
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
Sorry about the double send, David. I forgot to switch to reply-all in the gmail interface. On Tue, Jun 14, 2011 at 11:49 AM, wrote: > You absolutely still can use FunctionalDependencies to determine type > equality in GHC 7. For example, I just verified the code below with > GHC 7.02: > > *Main> typeEq True False > HTrue > *Main> typeEq (1 :: Int) (2 :: Int) > HTrue > *Main> typeEq (1 :: Int) False > HFalse > > As always, you have to make sure one of the overlapping instances is > more specific than the other, which you can do by substituting a > parameter c for HFalse in the false case and fixing c to HFalse using > another class like TypeCast in the context. (As contexts play no role > in instance selection, they don't make the instance any more > specific.) > > While I don't have convenient access to GHC 6 right this second, I'm > pretty sure there has been no change for a while, as the HList paper > discussed this topic in 2004. Okay. I don't really write a lot of code like this, so maybe I missed the quirks. In that case, HList has been relying on broken behavior of fundeps for 7 years. :) Because the instance: instance TypeEq a b c violates the functional dependency, by declaring: instance TypeEq Int Int Int instance TypeEq Int Int Char instance TypeEq Int Int Double ... instance TypeEq Int Char Int instance TypeEq Int Char Char ... and adding the constraint doesn't actually affect which instances are being declared, it just adds a constraint requirement for when any of the instances are used. It appears I was wrong, though. GHC doesn't actually fix the instance for such fundeps, and the following compiles and runs fine: class C a b | a -> b where foo :: a -> b foo = error "Yo dawg." instance C a b where bar :: Int bar = foo "x" baz :: Char baz = foo "x" so we're using an instance C String Int and an instance C String Char despite the fact that there's a functional dependency from the first argument to the second. -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
At Tue, 14 Jun 2011 10:40:48 -0400,
Dan Doel wrote:
>
> > 1. As things stand in GHC you can do some things with functional
> > dependencies that you can't do with type families. The archetypical example
> > is type equality. We cannot write
> > type family Eq a b :: *
> > type instance Eq k k = True
> > type instance Eq j k = False
> > because the two instances overlap. But you can with fundeps
> > class Eq a b c | a b -> c
> > instance Eq k k True
> > instance Eq j k False
> > As Alexey mentioned, fundeps have other disadvantages, so it's reasonable
> > to ask whether type families could extend to handle cases like this.
>
> Fundeps no longer allow this as of GHC 7, it seems. It causes the same
> fundep violation as the case:
>
> class C a b | a -> b
> instance C a R
> instance C T U
You absolutely still can use FunctionalDependencies to determine type
equality in GHC 7. For example, I just verified the code below with
GHC 7.02:
*Main> typeEq True False
HTrue
*Main> typeEq (1 :: Int) (2 :: Int)
HTrue
*Main> typeEq (1 :: Int) False
HFalse
As always, you have to make sure one of the overlapping instances is
more specific than the other, which you can do by substituting a
parameter c for HFalse in the false case and fixing c to HFalse using
another class like TypeCast in the context. (As contexts play no role
in instance selection, they don't make the instance any more
specific.)
While I don't have convenient access to GHC 6 right this second, I'm
pretty sure there has been no change for a while, as the HList paper
discussed this topic in 2004.
David
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class TypeCast a b | a -> b where
typeCast :: a -> b
instance TypeCast a a where
typeCast = id
data HTrue = HTrue deriving (Show)
data HFalse = HFalse deriving (Show)
class TypeEq a b c | a b -> c where
typeEq :: a -> b -> c
instance TypeEq a a HTrue where
typeEq _ _ = HTrue
instance (TypeCast HFalse c) => TypeEq a b c where
typeEq _ _ = typeCast HFalse
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
On Tue, Jun 14, 2011 at 11:27 AM, Andrea Vezzosi wrote: >> class C a b | a -> b >> instance C a R >> instance C T U > > Are you sure that worked before? 80% > The following still does anyhow: > > data R > data T > data U > class C a b | a -> b > instance TypeCast R b => C a b > instance TypeCast U b => C T b > > In fact this is how IsFunction was implemented in 2005[1], and the > same transformation appears to work for the Eq class too. > If we allow TypeFamilies we can use (~) instead of the TypeCast hack, > fortunately. So it does. instance (b ~ R) => C a b instance (b ~ U) => C T b Which is odd. I don't think there's a way to justify this working. Either the preconditions are being taken into account, in which case there is no reason for this to behave differently from: instance C a R instance C T U or the preconditions are not being taken into account (which is the type class way), in which case both of the qualified instances are illegal, because they declare instances C T b for all b (plus a constraint on the use), which violates the fundep. I've seen examples like this before, and I think what GHC ends up doing (now) is fixing the 'b' to whatever instance it needs first. But I don't think that's very good behavior. In this case it happens that it's impossible to use at more than one instance, but if you accept the instances, you're back to the questions of type soundness that are only evaded because fundeps don't actually use all the information they allegedly express. -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
At Tue, 14 Jun 2011 09:36:41 +, Simon Peyton-Jones wrote: > > 5. David wants a wiki page fixed. But which one? And how is it "locked > down"? This page: http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies Currently under cons for FunctionalDependencies, it says: AssociatedTypes seem to be more promising. I proposed the following fix: AssociatedTypes seem to be more promising, but in their current form are not as general as FunctionalDependencies [link]. where the link points to this or another email thread. Is there a policy that only a proposal's "owner" can modify the wiki page? Or that you have to be a member of the Haskell' committee? At any rate, when I log into the Haskell' wiki, I don't get an Edit button. That's all I meant by locked down. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
On Tue, Jun 14, 2011 at 4:40 PM, Dan Doel wrote:
> On Tue, Jun 14, 2011 at 5:36 AM, Simon Peyton-Jones
> wrote:
>> There was an interesting thread on haskell-prime [1], about the relationship
>> between functional dependencies and type families. This message is my
>> attempt to summarise the conclusions of that thread. I'm copying other
>> interested parties (eg Oleg, Dimitrios)
>> [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html
>>
>> 1. As things stand in GHC you can do some things with functional
>> dependencies that you can't do with type families. The archetypical example
>> is type equality. We cannot write
>> type family Eq a b :: *
>> type instance Eq k k = True
>> type instance Eq j k = False
>> because the two instances overlap. But you can with fundeps
>> class Eq a b c | a b -> c
>> instance Eq k k True
>> instance Eq j k False
>> As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to
>> ask whether type families could extend to handle cases like this.
>
> Fundeps no longer allow this as of GHC 7, it seems. It causes the same
> fundep violation as the case:
>
> class C a b | a -> b
> instance C a R
> instance C T U
Are you sure that worked before? The following still does anyhow:
{-# LANGUAGE MultiParamTypeClasses, OverlappingInstances,
FunctionalDependencies
, EmptyDataDecls, FlexibleInstances,
UndecidableInstances #-}
class TypeCast a b | a -> b, b->a where typeCast :: a -> b
class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x
data R
data T
data U
class C a b | a -> b
instance TypeCast R b => C a b
instance TypeCast U b => C T b
In fact this is how IsFunction was implemented in 2005[1], and the
same transformation appears to work for the Eq class too.
If we allow TypeFamilies we can use (~) instead of the TypeCast hack,
fortunately.
[1] http://okmij.org/ftp/Haskell/isFunction.lhs
-- Andrea
> for R /~ U. Which I find somewhat sensible, because the definitions
> together actually declare two relations for any type:
>
> Eq T T False
> Eq T T True
>
> and we are supposed to accept that because one is in scope, and has a
> particular form, the other doesn't exist. But they needn't always be
> in scope at the same time.
>
> Essentially, GHC 7 seems to have separated the issue of type-function
> overlapping, which is unsound unless you have specific conditions that
> make it safe---conditions which fundeps don't actually ensure (fundeps
> made it 'safe' in the past by not actually doing all the computation
> that type families do)---from the issue of instance overlapping, which
> is always sound at least. But if I'm not mistaken, type families can
> handle these cases.
>
> I'd personally say it's a step in the right direction, but it probably
> breaks a lot of HList-related stuff.
>
> -- Dan
>
> ___
> Haskell-prime mailing list
> Haskell-prime@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
>
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
On Tue, Jun 14, 2011 at 5:36 AM, Simon Peyton-Jones wrote: > There was an interesting thread on haskell-prime [1], about the relationship > between functional dependencies and type families. This message is my > attempt to summarise the conclusions of that thread. I'm copying other > interested parties (eg Oleg, Dimitrios) > [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html > > 1. As things stand in GHC you can do some things with functional dependencies > that you can't do with type families. The archetypical example is type > equality. We cannot write > type family Eq a b :: * > type instance Eq k k = True > type instance Eq j k = False > because the two instances overlap. But you can with fundeps > class Eq a b c | a b -> c > instance Eq k k True > instance Eq j k False > As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to > ask whether type families could extend to handle cases like this. Fundeps no longer allow this as of GHC 7, it seems. It causes the same fundep violation as the case: class C a b | a -> b instance C a R instance C T U for R /~ U. Which I find somewhat sensible, because the definitions together actually declare two relations for any type: Eq T T False Eq T T True and we are supposed to accept that because one is in scope, and has a particular form, the other doesn't exist. But they needn't always be in scope at the same time. Essentially, GHC 7 seems to have separated the issue of type-function overlapping, which is unsound unless you have specific conditions that make it safe---conditions which fundeps don't actually ensure (fundeps made it 'safe' in the past by not actually doing all the computation that type families do)---from the issue of instance overlapping, which is always sound at least. But if I'm not mistaken, type families can handle these cases. I'd personally say it's a step in the right direction, but it probably breaks a lot of HList-related stuff. -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies & type-level recursion
There was an interesting thread on haskell-prime [1], about the relationship between functional dependencies and type families. This message is my attempt to summarise the conclusions of that thread. I'm copying other interested parties (eg Oleg, Dimitrios) [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html 1. As things stand in GHC you can do some things with functional dependencies that you can't do with type families. The archetypical example is type equality. We cannot write type family Eq a b :: * type instance Eq k k = True type instance Eq j k = False because the two instances overlap. But you can with fundeps class Eq a b c | a b -> c instance Eq k k True instance Eq j k False As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to ask whether type families could extend to handle cases like this. 2. In a hypothetical extension to type families, namely *closed* type families, you could support overlap: closed type family Eq a b :: * where type instance Eq k k = True type instance Eq j k = False The idea is that you give all the equations together; matching is top-to-bottom; and the type inference only picks an equation when all the earlier equations are guaranteed not to match. So there is no danger of making different choices in different parts of the program (which is what gives rise to unsoundness). 3. Closed type families are not implemented yet. The only tricky point I see would be how to express in System FC the proof that "earlier equations don't match". Moreover, to support abstraction one might well want David's /~ predicate, so that you could say f :: forall a b. (a /~ b) => ..blah.. This f can be applied to any types a,b provided they don't match. I'm frankly unsure about all the consequences here. 4. As Roman points out, type families certainly do support recursion; it's just they don't support overlap. 5. David wants a wiki page fixed. But which one? And how is it "locked down"? 6. There is a very old Trac wiki page about "total" type families here http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies Written by Manuel, I think it needs updating. That's my summary! Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
