ll-users@haskell.org
| Subject: GADTs and functional dependencies in ghc 6.10.1
|
| Hello all,
|
| I think (hope) this question is different from the ones about GADTs
| recently discussed on this list. The following program compiles under
| ghc 6.8.2 but not under ghc 6.10.1:
|
| > {-# LANGUAG
Hello all,
I think (hope) this question is different from the ones about GADTs
recently discussed on this list. The following program compiles under
ghc 6.8.2 but not under ghc 6.10.1:
> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GADTs,
> KindSignatures, ScopedTypeVariables #-}
| while both GHC and Hugs accept this variation:
|
| class FD a b | a -> b
| f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
| f x y = undefined
|
| and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'.
|
| So they use the FD globally (when checking use of 'f'), but not local
By "global" I really meant "throughout the scope of the type variable concerned.
Nevertheless, the program you give is rejected, even though the scope is global:
class FD a b | a -> b
f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
f x y = y
Both GHC and Hugs erroneously reject the program,
w
o:[EMAIL PROTECTED]
| Sent: 24 September 2008 19:27
| To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
| Subject: Re: GADTs and functional dependencies
|
| >> This has never worked with fundeps, because it involves a *local* type
| equality (one that holds
| >> in some places
This has never worked with fundeps, because it involves a *local* type equality (one that holds
in some places and not others) and my implementation of fundeps is fundamentally based on
*global* equality. Prior to GADTs that was fine!
Actually, how does that relate to reasoning under assumptio
Hello Simon,
thank you for your extensive answer!
I think, I’ll try to work around the fundep deficiencies and if that doesn’t
work, switch to type families.
But your answer raised further questions/comments:
> class (F a ~ b) => C a b
> type family F a
>
> (Note for 6.10 use
This has never worked with fundeps, because it involves a *local* type equality (one that holds in
some places and not others) and my implementation of fundeps is fundamentally based on *global*
equality. Prior to GADTs that was fine!
Thanks for the explanation, Simon - it clears up some outst
Wolfgang writes
| > data GADT a where
| >
| > GADT :: GADT ()
| >
| > class Class a b | a -> b
| >
| > instance Class () ()
| >
| > fun :: (Class a b) => GADT a -> b
| > fun GADT = ()
You're right that this program should typecheck. In the case branch we
discover (locally) that a~(), and he
Am Mittwoch, 24. September 2008 15:11 schrieb Ian Lynagh:
> On Wed, Sep 24, 2008 at 12:55:29PM +0200, Wolfgang Jeltsch wrote:
> > I thought, someone said that with the new typing machinery in GHC 6.10,
> > more functional dependency programs are accepted because functional
> > dependencies are hand
On Wed, Sep 24, 2008 at 12:55:29PM +0200, Wolfgang Jeltsch wrote:
>
> I thought, someone said that with the new typing machinery in GHC 6.10, more
> functional dependency programs are accepted because functional dependencies
> are handled similarly to type families (or something like that). Is
Am Dienstag, 23. September 2008 19:07 schrieben Sie:
> >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
> >>
> >> data GADT a where
> >>
> >> GADT :: GADT ()
> >>
> >> class Class a b | a -> b
> >>
> >> instance Class () ()
> >>
> >> fun :: (Class a b) => GADT a -> b
> >
On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz
<[EMAIL PROTECTED]> wrote:
> You cannot create a normal function "fun". You can make a type class
> function
>
> fun :: Class a b => GADT a -> b
>
>> data GADT a where
>> GADT :: GADT ()
>> GADT2 :: GADT String
>>
>> -- fun1 :: GADT () -> ()
You cannot create a normal function "fun". You can make a type class function
fun :: Class a b => GADT a -> b
data GADT a where
GADT :: GADT ()
GADT2 :: GADT String
-- fun1 :: GADT () -> () -- infers type
fun1 g = case g of
(GADT :: GADT ()) -> ()
-- fun2 :: GADT String
On Tue, Sep 23, 2008 at 9:07 AM, Wolfgang Jeltsch
<[EMAIL PROTECTED]> wrote:
> Hello,
>
> please consider the following code:
>
>> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
>>
>> data GADT a where
>>
>> GADT :: GADT ()
>>
>> class Class a b | a -> b
>>
>> instance Cl
On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch
<[EMAIL PROTECTED]> wrote:
> Am Dienstag, 23. September 2008 18:19 schrieben Sie:
>> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
>>
>> <[EMAIL PROTECTED]> wrote:
>> > Hello,
>> >
>> > please consider the following code:
>> >> {-# LANGUAGE GADT
On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch
<[EMAIL PROTECTED]> wrote:
> Am Dienstag, 23. September 2008 18:19 schrieben Sie:
>> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
>>
>> <[EMAIL PROTECTED]> wrote:
>> > Hello,
>> >
>> > please consider the following code:
>> >> {-# LANGUAGE GADT
On Tue, Sep 23, 2008 at 6:36 PM, Wolfgang Jeltsch
<[EMAIL PROTECTED]> wrote:
> Pattern matching against the data constructor GADT specializes a to (). Since
> Class uses a functional dependency, it is clear that b has to be ().
True, but it wont work if you provide () as the result and b in the
e
Am Dienstag, 23. September 2008 18:19 schrieben Sie:
> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
>
> <[EMAIL PROTECTED]> wrote:
> > Hello,
> >
> > please consider the following code:
> >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
> >>
> >> data GADT a where
> >>
On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
<[EMAIL PROTECTED]> wrote:
> Hello,
>
> please consider the following code:
>
>> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
>>
>> data GADT a where
>>
>> GADT :: GADT ()
>>
>> class Class a b | a -> b
>>
>> instance Cl
Hello,
please consider the following code:
> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
>
> data GADT a where
>
> GADT :: GADT ()
>
> class Class a b | a -> b
>
> instance Class () ()
>
> fun :: (Class a b) => GADT a -> b
> fun GADT = ()
I’d expect this to wor
21 matches
Mail list logo
