A list to discuss Haskell', the next revision of the programming language Haskell. ()

Dan Doel | 14 Jun 2011 18:31

Picon

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,
<dm-list-haskell-prime@...> 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.

(Continue reading)

Andrea Vezzosi | 14 Jun 2011 18:59

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

On Tue, Jun 14, 2011 at 6:31 PM, Dan Doel <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,
> <dm-list-haskell-prime@...> 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.

(Continue reading)

dm | 14 Jun 2011 19:19

Picon

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."
>

(Continue reading)

Dan Doel | 14 Jun 2011 21:09

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

On Tue, Jun 14, 2011 at 1:19 PM,
<dm-list-haskell-prime@...> 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.

(Continue reading)

dm | 14 Jun 2011 23:38

Picon

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,
> <dm-list-haskell-prime <at> scs.stanford.edu> 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

(Continue reading)

Simon Peyton-Jones | 15 Jun 2011 00:20

Picon

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]

(Continue reading)

Dan Doel | 15 Jun 2011 01:21

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

On Tue, Jun 14, 2011 at 5:38 PM,
<dm-list-haskell-prime@...> 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:

(Continue reading)

dm | 15 Jun 2011 03:56

Picon

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

(Continue reading)

Simon Peyton-Jones | 15 Jun 2011 12:36

Picon

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

| 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. 

The issue doesn't even arise with type families:

	class MonadState m where
	  type State m :: *

	instance MonadState m => MonadState (MaybeT m) where
	  type State (MaybeT m) = State m

So examples that fail the coverage condition in fundeps, but (as you argue) are ok because the context
expresses the dependency, are sometimes just fine with type families.

|  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)

(Continue reading)

Ben Millwood | 15 Jun 2011 14:58

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

On Wed, Jun 15, 2011 at 11:36 AM, Simon Peyton-Jones
<simonpj@...> wrote:
> |       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
>
> Why do you need the first instance?  Isn't the second sufficient for (StateT s m) as well?
>
> Simon
>

The second will define /an/ instance for StateT s m, but it'll be the
wrong one :) the second instance says 'pass the responsibility for
dealing with state to the transformed monad', whereas the StateT wants
to deal with the state itself.

dm | 15 Jun 2011 18:13

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

At Wed, 15 Jun 2011 10:36:46 +0000,
Simon Peyton-Jones wrote:
> 
> The issue doesn't even arise with type families:
> 
> 	class MonadState m where
> 	  type State m :: *
> 
> 	instance MonadState m => MonadState (MaybeT m) where
> 	  type State (MaybeT m) = State m
> 
> So examples that fail the coverage condition in fundeps, but (as you argue) are ok because the context
expresses the dependency, are sometimes just fine with type families.

Sorry, I guess that specific example works.  It's the other one (which
saves the programmer from having to define N^2 instances) that can
never work with type families.

> |  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

(Continue reading)

Dan Doel | 16 Jun 2011 02:48

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

On Tue, Jun 14, 2011 at 9:56 PM,
<dm-list-haskell-prime@...> wrote:
> 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 wasn't really posting in this thread because I'm confused about how
fundeps actually behave in GHC. Rather, I care about what functional
dependencies mean, and what they should do, not just what they do
actually do in one implementation or another.

> 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 know that the actual, current implementation won't violate type
safety. But there are reasonable expectations for how *functional
dependencies* might work that would cause problems. Here's an example.

    class C a b | a -> b

(Continue reading)

dm | 16 Jun 2011 05:08

Picon

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

At Wed, 15 Jun 2011 20:48:07 -0400,
Dan Doel wrote:
> 
> I know that the actual, current implementation won't violate type
> safety. But there are reasonable expectations for how *functional
> dependencies* might work that would cause problems. Here's an example.
> 
>     class C a b | a -> b
> 
>     instance C Int b
> 
>     foo :: forall a b c d. (C a c, C b d, a ~ b) => a -> b -> c -> d
>     foo _ _ x = x
> 
>     coerce :: forall a b. a -> b
>     coerce = foo (5 :: Int) (5 :: Int)
> 
> This currently gets complaints about not being able to deduce c ~ d.
> However, actually reading things as genuine functional dependencies,
> there's nothing wrong with the logic:

I don't understand how this code would work under any circumstances.
At the very least, you are missing a context for coerce and the type
of foo would have to be ... => a -> b -> c -> c.  If two types are the
same, you are not allowed to declare them to be different.

Also, it's easy to add a method of some class to do the coercion,
while it's hard to emulate polymorphic types if you don't have them.
So I'd say the current behavior is more useful--allowing massive code
reduction in some cases, while I'm not yet convinced of the utility of

(Continue reading)

Return

Return to gmane.comp.lang.haskell.prime.

Project Web Page

A list to discuss Haskell', the next revision of the programming language Haskell. ()

Search Archive

Language

Change language

Options

Current view: Threads only / Showing only 20 lines / Not hiding cited text.
Change to All messages, whole messages, or hide cited text.

Post a message
NNTP Newsgroup
Classic Gmane web interface
XML

XML

RSS Feed
List Information

About Gmane