Solved but strange error in type inference

AUGER Cédric

3 Jan 2012 3 Jan '12

4:43 a.m.

Hi all, I am an Haskell newbie; can someone explain me why there is no reported error in @legSome@ but there is one in @legSomeb@ (I used leksah as an IDE, and my compiler is: $ ghc -v Glasgow Haskell Compiler, Version 7.2.1, stage 2 booted by GHC version 6.12.3 ) What I do not understand is that the only difference was a typing anotation to help the type inference, but I believed that this annotation was already given by the signature I give, so I am quite lost. Thanks in advance! ====================================================================== {-# OPTIONS_GHC -XScopedTypeVariables #-} -- why isn't this option always enabled... {-# OPTIONS_GHC -XGADTs #-} import Data.Word import qualified Data.Map as M import qualified Data.Set as S data Symbols nt t = NT nt -- ^ non terminal | T t -- ^ terminal deriving (Eq, Ord) type Sem s = [s]->s data Rule nt t s = Rule { refined :: nt , expression :: [Symbols nt t] , emit :: Sem s } type RRule nt t s = ([Symbols nt t], Sem s) data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s]) legSome :: LegGram nt t s -> nt -> Either String ([t], s) -- ^^^^^^^^^^^^^^ -- isn't this redundant? -- vvvvvvvvvvvvvv legSome ((LegGram g)::LegGram nt t s) ntV = case M.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (M.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l legSomeb :: LegGram nt t s -> nt -> Either String ([t], s) -- but without it I have an error reported legSomeb (LegGram g) ntV = case M.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSomeb (LegGram (M.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

Show replies by date

Yves Parès

3 Jan 3 Jan

5:03 a.m.

Perhaps you should give us the error the compiler give you. Plus: data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s]) will become invalid. Currently, such class constraints are ignored. You should remove the 'Ord nt' constraint and add it to you legSome function. (Maybe that's a track to solve your problem...) You have also another solution: make your LegGram type available *for all*Ord nt (with GADTs or ExistentialQuantification), thus making you unable to know which type 'nt' exactly is: data LegGram t s = forall nt. Ord nt => LegGram (M.Map nt [RRule nt t s]) or data LegGram t s where LegGram :: Ord nt => M.Map nt [RRule nt t s] -> LegGram t s should be both valid. I tend to prefer the latter (the use of a GADT), as it makes you declare and handle your type constructor just like any function. But I don't know if it fits you requirements. 2012/1/3 AUGER Cédric

...

Hi all, I am an Haskell newbie; can someone explain me why there is no reported error in @legSome@ but there is one in @legSomeb@

(I used leksah as an IDE, and my compiler is: $ ghc -v Glasgow Haskell Compiler, Version 7.2.1, stage 2 booted by GHC version 6.12.3 )

What I do not understand is that the only difference was a typing anotation to help the type inference, but I believed that this annotation was already given by the signature I give, so I am quite lost.

Thanks in advance!

====================================================================== {-# OPTIONS_GHC -XScopedTypeVariables #-} -- why isn't this option always enabled...

{-# OPTIONS_GHC -XGADTs #-}

import Data.Word import qualified Data.Map as M import qualified Data.Set as S

data Symbols nt t = NT nt -- ^ non terminal | T t -- ^ terminal deriving (Eq, Ord)

type Sem s = [s]->s

data Rule nt t s = Rule { refined :: nt , expression :: [Symbols nt t] , emit :: Sem s }

type RRule nt t s = ([Symbols nt t], Sem s) data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s])

legSome :: LegGram nt t s -> nt -> Either String ([t], s) -- ^^^^^^^^^^^^^^ -- isn't this redundant? -- vvvvvvvvvvvvvv legSome ((LegGram g)::LegGram nt t s) ntV = case M.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (M.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

legSomeb :: LegGram nt t s -> nt -> Either String ([t], s) -- but without it I have an error reported legSomeb (LegGram g) ntV = case M.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSomeb (LegGram (M.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yucheng Zhang

5:17 a.m.

On Tue, Jan 3, 2012 at 5:43 PM, AUGER Cédric wrote:

...

legSomeb :: LegGram nt t s -> nt -> Either String ([t], s) -- but without it I have an error reported legSomeb (LegGram g) ntV = case M.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSomeb (LegGram (M.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

I found it compiling well if removing this line: subsome :: [RRule nt t s] -> Either String ([t], s) It seems to me that the compiler is not sure the two 'nt' are equal. The ScopedTypeVariables can make the compiler believe they are equal.

Brandon Allbery

5:44 a.m.

On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang wrote:

...

subsome :: [RRule nt t s] -> Either String ([t], s)

It seems to me that the compiler is not sure the two 'nt' are equal. The ScopedTypeVariables can make the compiler believe they are equal.

But ScopedTypeVariables is enabled already. OTOH, I *think* the embedded Ord constraint is screwing things up (which is why it's showing up in the error message), because it's embedded and therefore has its own limited scope which prevents ScopedTypeVariables from doing the right thing. This idiosyncrasy is why those embedded constraints are being removed from the language except in more controllable and useful ways (namely GADTs; the H98 version is not capable of doing anything useful, as I understand it, it can only screw up typing in situations like this without actually adding anything useful to the type system, as it's not possible to bring the Ord constraint usefully into scope outside the data declaration itself). (More technically, and I think this is correct: the effective data type is (forall nt. Ord nt => LegGram (M.Map nt [RRule nt t s])) Note the outer parentheses; the Ord constraint is *only* active within those outer parentheses, meaning that it prevents the type of "nt" from matching that in any other use of the type, even in the same expression, even with ScopedTypeVariables.) -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Yucheng Zhang

5:50 a.m.

On Tue, Jan 3, 2012 at 6:44 PM, Brandon Allbery wrote:

...

On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang wrote:

...
subsome :: [RRule nt t s] -> Either String ([t], s)

It seems to me that the compiler is not sure the two 'nt' are equal. The ScopedTypeVariables can make the compiler believe they are equal.

But ScopedTypeVariables is enabled already.

Sorry, I meant actually using ScopedTypeVariables as in the first function, which compiles well: legSome :: LegGram nt t s -> nt -> Either String ([t], s) -- ^^^^^^^^^^^^^^ -- isn't this redundant? -- vvvvvvvvvvvvvv legSome ((LegGram g)::LegGram nt t s) ntV = case M.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (M.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

Brandon Allbery

6:23 a.m.

On Tue, Jan 3, 2012 at 05:50, Yucheng Zhang wrote:

...

On Tue, Jan 3, 2012 at 6:44 PM, Brandon Allbery wrote:

...
On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang wrote:

...
subsome :: [RRule nt t s] -> Either String ([t], s)

It seems to me that the compiler is not sure the two 'nt' are equal. The ScopedTypeVariables can make the compiler believe they are equal.

But ScopedTypeVariables is enabled already.

Sorry, I meant actually using ScopedTypeVariables as in the first function, which compiles well:

legSome :: LegGram nt t s -> nt -> Either String ([t], s)

Except he's not; an explicit "forall" is needed to indicate the type variables to be brought into scope. It would need to be

...

legSome :: forall nt t s. LegGram nt t s -> nt -> Either String ([t], s)

-- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Yucheng Zhang

6:35 a.m.

As I understand it, both ways work.

...

legSome ((LegGram g)::LegGram nt t s) ntV

If you compile this without ScopedTypeVariables extension, GHC will remind you of it:

...

Illegal signature in pattern: LegGram nt t s Use -XScopedTypeVariables to permit it

So another solution is to avoid the ugly redundancy is:

...

legSome :: forall nt t s . LegGram nt t s -> nt -> Either String ([t], s)

Yves Parès

6:43 a.m.

That is error-prone. Plus the code does not need ScopedTypeVariables. The real problem comes from the use of a class constraint on the LegGram data constructor. data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s]) Short answer: you *can't *add class constraints to an already declared type variable: The LegGram *type *constructor declares the 'nt' variable (and then brings it into scope), so trying afterwards to add a constraint to it for the LegGram *data *constructor is invalid, so the compiler understands this: data LegGram nt t s = *forall nt.* Ord nt => LegGram (M.Map *nt* [RRule *nt*t s]) ...the declaration and scoping of a *new* type variable. This is it, right? 2012/1/3 Yucheng Zhang

...

As I understand it, both ways work.

...
legSome ((LegGram g)::LegGram nt t s) ntV

If you compile this without ScopedTypeVariables extension, GHC will remind you of it:

...
Illegal signature in pattern: LegGram nt t s Use -XScopedTypeVariables to permit it

So another solution is to avoid the ugly redundancy is:

...
legSome :: forall nt t s . LegGram nt t s -> nt -> Either String ([t], s)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Brandon Allbery

6:49 a.m.

On Tue, Jan 3, 2012 at 06:43, Yves Parès wrote:

...

That is error-prone. Plus the code does not need ScopedTypeVariables. The real problem comes from the use of a class constraint on the LegGram data constructor.

data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s])

Short answer: you *can't *add class constraints to an already declared type variable:

The LegGram *type *constructor declares the 'nt' variable (and then brings it into scope), so trying afterwards to add a constraint to it for the LegGram *data *constructor is invalid, so the compiler understands this: data LegGram nt t s = *forall nt.* Ord nt => LegGram (M.Map *nt* [RRule * nt* t s]) ...the declaration and scoping of a *new* type variable.

This is it, right?

Yep, with the additional gotcha that two uses of the same data constructor in an expression will not unify those type variables because it's scoped to the data constructor itself. Which is the confusing and error-prone behavior that led to it being removed from the next version of the standard (probably; the proposal was accepted but H'2011 was bypassed and H'2012 has not yet started). -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Yves Parès

8:04 a.m.

...

two uses of the same data constructor in an expression will not unify those type variables because it's scoped to the data constructor itself

Which is somewhat clearer when using GADTs: data LegGram t s where LegGram :: Ord nt => M.Map nt [RRule nt t s] -> LegGram t s Here, as the LegGram data constructor is a function, it follows their rules, then is equivalent to: LegGram :: forall nt. Ord nt => M.Map nt [RRule nt t s] -> LegGram t s Which clearly indicated that 'nt' only exists within the scope of a variable. However, GADTs add some ambiguity: data LegGram *t* *s* where It's not easy for a beginner to see that those type variables are *not *the same than those: LegGram :: Ord nt => M.Map nt [RRule nt *t s*] -> LegGram *t s* So, for short: data Something a b c = ... -- ^ Regular ADT, a b and c are brought into scope data Something a b c where ... -- ^ GADT, a b and c *are not *scoped, their name is useless, their use is only to indicate the arity of the type constructor. But we have kinds for that. I find it misleading. To me, it should be compulsory to write: data Something :: * -> * -> * where ... would be better, but I believe it requires another language extension. 2012/1/3 Brandon Allbery

...

On Tue, Jan 3, 2012 at 06:43, Yves Parès wrote:

...
That is error-prone. Plus the code does not need ScopedTypeVariables. The real problem comes from the use of a class constraint on the LegGram data constructor.

data LegGram nt t s = Ord nt => LegGram (M.Map nt [RRule nt t s])

Short answer: you *can't *add class constraints to an already declared type variable:

The LegGram *type *constructor declares the 'nt' variable (and then brings it into scope), so trying afterwards to add a constraint to it for the LegGram *data *constructor is invalid, so the compiler understands this: data LegGram nt t s = *forall nt.* Ord nt => LegGram (M.Map *nt* [RRule * nt* t s]) ...the declaration and scoping of a *new* type variable.

This is it, right?

Yep, with the additional gotcha that two uses of the same data constructor in an expression will not unify those type variables because it's scoped to the data constructor itself. Which is the confusing and error-prone behavior that led to it being removed from the next version of the standard (probably; the proposal was accepted but H'2011 was bypassed and H'2012 has not yet started).

-- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Brandon Allbery

6:46 a.m.

On Tue, Jan 3, 2012 at 06:35, Yucheng Zhang wrote:

...

...
legSome ((LegGram g)::LegGram nt t s) ntV

If you compile this without ScopedTypeVariables extension, GHC will remind you of it:

...
Illegal signature in pattern: LegGram nt t s Use -XScopedTypeVariables to permit it

Right, but I think this is conflating two aspects of ScopedTypeVariables and may not bring them into scope "fully". Although, that's a question for someone who understands ghc's type system far better than I do. -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Yucheng Zhang

6:49 a.m.

On Tue, Jan 3, 2012 at 7:46 PM, Brandon Allbery wrote:

...

Right, but I think this is conflating two aspects of ScopedTypeVariables and may not bring them into scope "fully". Although, that's a question for someone who understands ghc's type system far better than I do.

I found some descriptions of ScopedTypeVariables here: http://hackage.haskell.org/trac/haskell-prime/wiki/ScopedTypeVariables

Yucheng Zhang

7:24 a.m.

On Tue, Jan 3, 2012 at 7:49 PM, Yucheng Zhang wrote:

...

I found some descriptions of ScopedTypeVariables here:

http://hackage.haskell.org/trac/haskell-prime/wiki/ScopedTypeVariables

Sorry, I found just now a more up-to-date description in the GHC documentation: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension...

AUGER Cédric

8:23 a.m.

Thanks all, I finally give up to put Ord in the LegGram type. What was annoying me was that @legsome@ was in fact an instance of a class I defined. So I changed its signature to make it depend on Ord. That is not very nice, since at first glance, there could be implementations which does not require "nt" to be ordered. But as in some other method of this class I need it, I guess it isn't that annoying. I still do find the reported error strange, but thanks to your remarks, I can remove some typing annotation in the body of the function (which I forgot to remove and used while I was debugging my types) to avoid this ugly redundancy (I guess I could also remove the global type signature, but I like to keep them).

Yucheng Zhang

11:15 a.m.

As I investigated the code more carefully, I found that the type unification failure may not be related to the suspected class constraint on data constructor. I have made minor changes to the original code to remove the Ord constraint, including introducing a FakedMap with no requirement on Ord. The type unification failure continues:

...

Couldn't match type `nt1' with `nt' `nt1' is a rigid type variable bound by the type signature for subsome :: [RRule nt1 t1 s1] -> Either String ([t1], s1) at xx.hs:34:19 `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s) at xx.hs:29:1 Expected type: [Symbols nt1 t1] Actual type: [Symbols nt t] In the first argument of `makeWord', namely `r' In the expression: makeWord r

The complete changed code follows: data Symbols nt t = NT nt -- ^ non terminal | T t -- ^ terminal deriving (Eq, Ord) type Sem s = [s]->s data Rule nt t s = Rule { refined :: nt , expression :: [Symbols nt t] , emit :: Sem s } type RRule nt t s = ([Symbols nt t], Sem s) data FakedMap a b = FakedMap delete :: k -> FakedMap k a -> FakedMap k a delete a b = b lookup :: k -> FakedMap k a -> Maybe a lookup a b = Nothing data LegGram nt t s = LegGram (FakedMap nt [RRule nt t s]) legSome :: LegGram nt t s -> nt -> Either String ([t], s) legSome (LegGram g) ntV = case Main.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (Main.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

Yves Parès

11:44 a.m.

Remove subsome type signature. You are redeclaring type variables which obviously cannot match those of legSome. This cannot work without scoped type variables (and ad-hoc foralls to bring them to scope, of course). 2012/1/3 Yucheng Zhang

...

As I investigated the code more carefully, I found that the type unification failure may not be related to the suspected class constraint on data constructor.

I have made minor changes to the original code to remove the Ord constraint, including introducing a FakedMap with no requirement on Ord. The type unification failure continues:

...
Couldn't match type `nt1' with `nt' `nt1' is a rigid type variable bound by the type signature for subsome :: [RRule nt1 t1 s1] -> Either String ([t1], s1) at xx.hs:34:19 `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s) at xx.hs:29:1 Expected type: [Symbols nt1 t1] Actual type: [Symbols nt t] In the first argument of `makeWord', namely `r' In the expression: makeWord r

The complete changed code follows:

data Symbols nt t = NT nt -- ^ non terminal | T t -- ^ terminal deriving (Eq, Ord)

type Sem s = [s]->s

data Rule nt t s = Rule { refined :: nt , expression :: [Symbols nt t] , emit :: Sem s }

type RRule nt t s = ([Symbols nt t], Sem s)

data FakedMap a b = FakedMap

delete :: k -> FakedMap k a -> FakedMap k a delete a b = b

lookup :: k -> FakedMap k a -> Maybe a lookup a b = Nothing

data LegGram nt t s = LegGram (FakedMap nt [RRule nt t s])

legSome :: LegGram nt t s -> nt -> Either String ([t], s) legSome (LegGram g) ntV = case Main.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (Main.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Brent Yorgey

11:58 a.m.

The other much simpler solution no one has mentioned yet is to just pull 'subsome' out as its own top-level declaration. Having such a big function nested locally within a 'let' is ugly anyway, and it makes it harder to test and debug than necessary. -Brent On Tue, Jan 03, 2012 at 05:44:01PM +0100, Yves Parès wrote:

...

Remove subsome type signature. You are redeclaring type variables which obviously cannot match those of legSome. This cannot work without scoped type variables (and ad-hoc foralls to bring them to scope, of course).

2012/1/3 Yucheng Zhang

...
As I investigated the code more carefully, I found that the type unification failure may not be related to the suspected class constraint on data constructor.

I have made minor changes to the original code to remove the Ord constraint, including introducing a FakedMap with no requirement on Ord. The type unification failure continues:

...
Couldn't match type `nt1' with `nt' `nt1' is a rigid type variable bound by the type signature for subsome :: [RRule nt1 t1 s1] -> Either String ([t1], s1) at xx.hs:34:19 `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s) at xx.hs:29:1 Expected type: [Symbols nt1 t1] Actual type: [Symbols nt t] In the first argument of `makeWord', namely `r' In the expression: makeWord r

The complete changed code follows:

data Symbols nt t = NT nt -- ^ non terminal | T t -- ^ terminal deriving (Eq, Ord)

type Sem s = [s]->s

data Rule nt t s = Rule { refined :: nt , expression :: [Symbols nt t] , emit :: Sem s }

type RRule nt t s = ([Symbols nt t], Sem s)

data FakedMap a b = FakedMap

delete :: k -> FakedMap k a -> FakedMap k a delete a b = b

lookup :: k -> FakedMap k a -> Maybe a lookup a b = Nothing

data LegGram nt t s = LegGram (FakedMap nt [RRule nt t s])

legSome :: LegGram nt t s -> nt -> Either String ([t], s) legSome (LegGram g) ntV = case Main.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (Main.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s) subsome [] = Left "No word accepted!" subsome ((r,sem):l) = let makeWord [] = Right ([],[]) makeWord ((NT nnt):ll) = do (m, ss) <- sg nnt (mm, sss) <- makeWord ll return (m++mm, ss:sss) makeWord ((T tt):ll) = do (mm, sss) <- makeWord ll return (tt:mm, sss) in case makeWord r of Right (ll, mm) -> Right (ll, sem mm) Left err -> subsome l in subsome l

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

...

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yucheng Zhang

12:01 p.m.

On Wed, Jan 4, 2012 at 12:44 AM, Yves Parès wrote:

...

Remove subsome type signature. You are redeclaring type variables which obviously cannot match those of legSome. This cannot work without scoped type variables (and ad-hoc foralls to bring them to scope, of course).

That subsome type signature is from the original code. I wonder why the redeclared type variables cannot match those of legSome? p.s. I just realized that my changed code missed the line:

...

import qualified Data.Map as M

Yves Parès

12:07 p.m.

Brent is right. Separating functions is nicer to read and cleaner. Plus it enhances testability.

...

I wonder why the redeclared type variables cannot match those of legSome? Try to put a totally wrong type to subsome, like subsome :: Int and tell us from the error what type is actually inferred.

2012/1/3 Yucheng Zhang

...

On Wed, Jan 4, 2012 at 12:44 AM, Yves Parès wrote:

...
Remove subsome type signature. You are redeclaring type variables which obviously cannot match those of legSome. This cannot work without scoped type variables (and ad-hoc foralls to bring them to scope, of course).

That subsome type signature is from the original code.

I wonder why the redeclared type variables cannot match those of legSome?

p.s. I just realized that my changed code missed the line:

...
import qualified Data.Map as M

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yucheng Zhang

12:38 p.m.

On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès wrote:

...

Try to put a totally wrong type to subsome, like subsome :: Int and tell us from the error what type is actually inferred.

The error is like

...

Couldn't match type `nt' with `Int' `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s) at xx.hs:35:1 Expected type: [RRule Int t s] Actual type: [RRule nt t s] In the first argument of `subsome', namely `l' In the expression: subsome l

However, this error cannot be resolved by a use of ScopedTypeVariable, while the original error can be resolved. I still don't see where the mismatch happens in the original error. Any help is appreciated.

Yucheng Zhang

12:44 p.m.

On Wed, Jan 4, 2012 at 1:38 AM, Yucheng Zhang wrote:

...

On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès wrote:

...
Try to put a totally wrong type to subsome, like subsome :: Int and tell us from the error what type is actually inferred.

Sorry, I found I misunderstood the suggestion. I will try.

Yucheng Zhang

1:05 p.m.

On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès wrote:

...

...
I wonder why the redeclared type variables cannot match those of legSome? Try to put a totally wrong type to subsome, like subsome :: Int and tell us from the error what type is actually inferred.

The actually inferred type is Couldn't match expected type `Int' with actual type `[([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0)' In the expression: subsome :: Int I still don't understand why the original mismatch happens.

Bardur Arantsson

1:48 p.m.

...

2012/1/3 Yucheng Zhang

(Hopefully being a little more explicit about this can help you understand where things are going wrong.) [--snip--]

...

legSome :: LegGram nt t s -> nt -> Either String ([t], s)

The 'nt' you see above

...

legSome (LegGram g) ntV = case Main.lookup ntV g of Nothing -> Left "No word accepted!" Just l -> let sg = legSome (LegGram (Main.delete ntV g)) subsome :: [RRule nt t s] -> Either String ([t], s)

... isn't the same as the 'nt' you see in this line, so it constrains 'subsome' to a different type than the one you intended -- and indeed one which can't be unified with the inferred type. (Unless you use ScopedTypeVariables.) As Brent suggested, you should probably pull the "subsome" function out into a top-level function in any case. Cheers,

Yucheng Zhang

1:53 p.m.

On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson wrote:

...

'subsome' to a different type than the one you intended -- and indeed one which can't be unified with the inferred type. (Unless you use ScopedTypeVariables.)

Thanks for the reply. Actually, my question is why the different type can't be unified with the inferred type? Could you point me some related resources?

Yves Parès

2:46 p.m.

...

Actually, my question is why the different type can't be unified with the inferred type?

Because without ScopedTypeVariable, both types got expanded to : legSome :: *forall nt* t s. LegGram nt t s -> nt -> Either String ([t], s) subsome :: *forall nt* t s. [RRule nt t s] -> Either String ([t], s) So you see subsome declare new variables, which *do not *match the *rigid *ones declared by legSome signature, hence the incompatibility. As we said before, you have three ways to work it out: 1) Use scoped type variables with explicit forall nt on legSome and *no forall *on subsome, so that nt in subsome matches nt declared in legSome. 2) Don't give a type signature for subsome and let GHC find out which is its correct type. 3) Extract subsome so that it becomes a top-level function with a polymorphic type (Recommended). Now, concerning the error I asked you to deliberately provoke, that's the quickest way I found to know what is the output of the type inferer, and maybe the only simple one. So this error is:

...

Couldn't match expected type `Int' with actual type `[([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0)' In the expression: subsome :: Int GHC tells you the type it infers for subsome: [([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0) The nt you see is the one from legSome, those messages show scoped variables. (You'd get something like 'nt1' or 'nt0' if it was another variable, meant to be instanciated to a different type). This accords with your previous error message, which happens to give you more details about where the rigid type variable nt comes from: `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s)

HTH. 2012/1/3 Yucheng Zhang

...

On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson wrote:

...
'subsome' to a different type than the one you intended -- and indeed one which can't be unified with the inferred type. (Unless you use ScopedTypeVariables.)

Thanks for the reply.

Actually, my question is why the different type can't be unified with the inferred type? Could you point me some related resources?

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

AUGER Cédric

4 Jan 4 Jan

5:50 a.m.

Le Tue, 3 Jan 2012 20:46:15 +0100, Yves Parès a écrit :

...

...
Actually, my question is why the different type can't be unified with the inferred type?

Because without ScopedTypeVariable, both types got expanded to :

legSome :: *forall nt* t s. LegGram nt t s -> nt -> Either String ([t], s)

subsome :: *forall nt* t s. [RRule nt t s] -> Either String ([t], s)

So you see subsome declare new variables, which *do not *match the *rigid *ones declared by legSome signature, hence the incompatibility.

How ugly! I thought that Haskell didn't allow to mask type variables. Does that mean that I can do: foo :: (a -> a) -> (b -> b) -> a -> a foo bar dummy = let strange :: a -> a strange = dummy in foo (ok, that's dead code, but how misleading it would be!) Is there some way to enforce a typing error here? (I am pretty sure there is some flag to have explicit 'forall's, but I am not sure that it forces you to use 'forall' explicitely.) I come from Coq community (where forall must be explicit) and Ocaml community (where most people strongly rely on type inference and do not put types very often). I didn't try this example on Ocaml.

...

As we said before, you have three ways to work it out: 1) Use scoped type variables with explicit forall nt on legSome and *no forall *on subsome, so that nt in subsome matches nt declared in legSome. 2) Don't give a type signature for subsome and let GHC find out which is its correct type. 3) Extract subsome so that it becomes a top-level function with a polymorphic type (Recommended).

In fact I first wanted to write directly the method without using auxiliary functions (I changed my mind since, as I redisigned my code and it wasn't possible [or at least natural for me] to put the code directly inlined). In fact I often do nested functions when there are free variables in the function. I particulary hate to have code like that: foo :: bar -> foobar -> barfoo foo b fb = if f b fb then foo b (g b fb) else h b fb as b is in fact invariant in the calls of 'foo'; so I always rewrite this as: foo :: bar -> foobar -> barfoo foo b = let fooAux :: foobar -> barfoo fooAux fb = if f b fb then fooAux (g b fb) else h b fb in fooAux that is more verbose, but I well see what are the recursive parameters, and I have the (probably wrong) feeling that it is better since function calls have less arguments. Here subsome was depending on the free variable "sg", so I had to generalize it to do so even if I won't have benefits in having the ability to use it elsewhere (as it was the only place I wanted to use it). I always prefer to minimize the number of specialized functions, since I hate jumping from parts of code to other parts of code to understand what a function really does.

...

Now, concerning the error I asked you to deliberately provoke, that's the quickest way I found to know what is the output of the type inferer, and maybe the only simple one. So this error is:

...
Couldn't match expected type `Int' with actual type `[([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0)' In the expression: subsome :: Int GHC tells you the type it infers for subsome: [([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0) The nt you see is the one from legSome, those messages show scoped variables. (You'd get something like 'nt1' or 'nt0' if it was another variable, meant to be instanciated to a different type). This accords with your previous error message, which happens to give you more details about where the rigid type variable nt comes from: `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s)

HTH.

2012/1/3 Yucheng Zhang

...
On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson wrote:

...
'subsome' to a different type than the one you intended -- and indeed one which can't be unified with the inferred type. (Unless you use ScopedTypeVariables.)

Thanks for the reply.

Actually, my question is why the different type can't be unified with the inferred type? Could you point me some related resources?

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yves Parès

6:04 a.m.

...

Ocaml community (where most people strongly rely on type inference and do not put types very often)

Well it's the same for Haskell.

...

foo :: bar -> foobar -> barfoo foo b = let *fooAux :: foobar -> barfoo* -- You can comment it out fooAux fb = if f b fb then fooAux (g b fb) else h b fb in fooAux

Yes, I also like to write it that way, except you can *remove *fooAux type signature, and let GHC type inferer do its job, like in OCaml. Plus, 'foo' signature is merely documentation for you in that case.

...

I always prefer to minimize the number of specialized functions, since I hate jumping from parts of code to other parts of code to understand what a function really does.

Too bad, that's one of the assets of functional programming. The more splitted you design your functions, the easier it is to reuse and test them afterwards. A good practice in C-like languages also, IMHO. You can just write subsome right under legSome, it doesn't break legibility, and if you think it's best tell your module to export only legSome. ...Or, remove/comment the inner type signatures ;) 2012/1/4 AUGER Cédric

...

Le Tue, 3 Jan 2012 20:46:15 +0100, Yves Parès a écrit :

...
...
Actually, my question is why the different type can't be unified with the inferred type?

Because without ScopedTypeVariable, both types got expanded to :

legSome :: *forall nt* t s. LegGram nt t s -> nt -> Either String ([t], s)

subsome :: *forall nt* t s. [RRule nt t s] -> Either String ([t], s)

So you see subsome declare new variables, which *do not *match the *rigid *ones declared by legSome signature, hence the incompatibility.

How ugly! I thought that Haskell didn't allow to mask type variables.

Does that mean that I can do:

foo :: (a -> a) -> (b -> b) -> a -> a foo bar dummy = let strange :: a -> a strange = dummy in foo

(ok, that's dead code, but how misleading it would be!)

Is there some way to enforce a typing error here? (I am pretty sure there is some flag to have explicit 'forall's, but I am not sure that it forces you to use 'forall' explicitely.)

I come from Coq community (where forall must be explicit) and Ocaml community (where most people strongly rely on type inference and do not put types very often). I didn't try this example on Ocaml.

...
As we said before, you have three ways to work it out: 1) Use scoped type variables with explicit forall nt on legSome and *no forall *on subsome, so that nt in subsome matches nt declared in legSome. 2) Don't give a type signature for subsome and let GHC find out which is its correct type. 3) Extract subsome so that it becomes a top-level function with a polymorphic type (Recommended).

In fact I first wanted to write directly the method without using auxiliary functions (I changed my mind since, as I redisigned my code and it wasn't possible [or at least natural for me] to put the code directly inlined).

In fact I often do nested functions when there are free variables in the function. I particulary hate to have code like that:

foo :: bar -> foobar -> barfoo foo b fb = if f b fb then foo b (g b fb) else h b fb

as b is in fact invariant in the calls of 'foo'; so I always rewrite this as:

foo :: bar -> foobar -> barfoo foo b = let fooAux :: foobar -> barfoo fooAux fb = if f b fb then fooAux (g b fb) else h b fb in fooAux

that is more verbose, but I well see what are the recursive parameters, and I have the (probably wrong) feeling that it is better since function calls have less arguments.

Here subsome was depending on the free variable "sg", so I had to generalize it to do so even if I won't have benefits in having the ability to use it elsewhere (as it was the only place I wanted to use it).

I always prefer to minimize the number of specialized functions, since I hate jumping from parts of code to other parts of code to understand what a function really does.

...
Now, concerning the error I asked you to deliberately provoke, that's the quickest way I found to know what is the output of the type inferer, and maybe the only simple one. So this error is:

...
Couldn't match expected type `Int' with actual type `[([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0)' In the expression: subsome :: Int GHC tells you the type it infers for subsome: [([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0) The nt you see is the one from legSome, those messages show scoped variables. (You'd get something like 'nt1' or 'nt0' if it was another variable, meant to be instanciated to a different type). This accords with your previous error message, which happens to give you more details about where the rigid type variable nt comes from: `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s)

HTH.

2012/1/3 Yucheng Zhang

...
On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson wrote:

...
'subsome' to a different type than the one you intended -- and indeed one which can't be unified with the inferred type. (Unless you use ScopedTypeVariables.)

Thanks for the reply.

Actually, my question is why the different type can't be unified with the inferred type? Could you point me some related resources?

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yucheng Zhang

6:35 a.m.

On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès wrote:

...

Because without ScopedTypeVariable, both types got expanded to :

legSome :: forall nt t s. LegGram nt t s -> nt -> Either String ([t], s)

subsome :: forall nt t s. [RRule nt t s] -> Either String ([t], s)

So you see subsome declare new variables, which do not match the rigid ones declared by legSome signature, hence the incompatibility.

It's not obvious to see the incompatibility. I looked into the Haskell 2010 Language Report, and found my question answered in Section 4.4.1, along with a minimal reproducing example: f :: a -> a f x = x :: a -- invalid The confusing point to me is that the 'a' from 'f' type signature on its own is not universally quantified as I expected, and it is dependent on the type of 'f'. This dependence is not obvious for a beginner like me. ScopedTypeVariables will help to express the dependence exactly. And moving 'subsome' to top-level will prevent from bringing in the dependent type.

...

Now, concerning the error I asked you to deliberately provoke, that's the quickest way I found to know what is the output of the type inferer, and maybe the only simple one.

I find this one of the most interesting tricks I've seen.

Yves Parès

6:58 a.m.

...

f :: a -> a f x = x :: a -- invalid

Perfect example indeed.

...

The confusing point to me is that the 'a' from 'f' type signature on its own is not universally quantified as I expected, and it is dependent on the type of 'f'.

...

This dependence is not obvious for a beginner like me.

It's indeed counterintuitive, as you'd expect type variables to be scoped, but just note that: You have only *one *simple rule to remember: "*All* type variables appearing in a type expression get automatically* universally *quantified at the *beginning *of this expression". Practically : *When you see an type variable v, then GHC automatically puts a 'forall v' at the beginning of the whole expression.* No exceptions done, no ambiguity at all as long as ScopedTypeVariables stays unactivated. Following this one rule, it's clear that the example above cannot but become: f :: forall a. a -> a f x = x :: forall a. a Which is obviously wrong: when you *have entered* f, x has been instatiated to a specific type 'a', and then you want it to x to be of *any *type? That doesn't make sense.* **It's only logical. * 2012/1/4 Yucheng Zhang

...

On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès wrote:

...
Because without ScopedTypeVariable, both types got expanded to :

legSome :: forall nt t s. LegGram nt t s -> nt -> Either String ([t], s)

subsome :: forall nt t s. [RRule nt t s] -> Either String ([t], s)

So you see subsome declare new variables, which do not match the rigid ones declared by legSome signature, hence the incompatibility.

It's not obvious to see the incompatibility. I looked into the Haskell 2010 Language Report, and found my question answered in Section 4.4.1, along with a minimal reproducing example:

f :: a -> a f x = x :: a -- invalid

The confusing point to me is that the 'a' from 'f' type signature on its own is not universally quantified as I expected, and it is dependent on the type of 'f'.

This dependence is not obvious for a beginner like me.

ScopedTypeVariables will help to express the dependence exactly. And moving 'subsome' to top-level will prevent from bringing in the dependent type.

...
Now, concerning the error I asked you to deliberately provoke, that's the quickest way I found to know what is the output of the type inferer, and maybe the only simple one.

I find this one of the most interesting tricks I've seen.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yucheng Zhang

7:15 a.m.

On Wed, Jan 4, 2012 at 7:58 PM, Yves Parès wrote:

...

f :: forall a. a -> a f x = x :: forall a. a

Which is obviously wrong: when you have entered f, x has been instatiated to a specific type 'a', and then you want it to x to be of any type? That doesn't make sense.

I did not expect the type variables to be scoped. I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem.

Yucheng Zhang

7:59 a.m.

On Wed, Jan 4, 2012 at 8:15 PM, Yucheng Zhang wrote:

...

I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem.

I've never been thinking in a detailed level, and the 'x' appears to be able to take any type, and thus the wrong expectation. Thanks for all the input from all.

AUGER Cédric

8:57 a.m.

So is there anyway to "force" the scoping of variables, so that f :: a -> a f x = x :: a becomes valid? Do we need to do it the Ocaml way, that is not declaring the first line, activate XScopedVariables and do: f :: a -> a = \x -> x :: a or f (x :: a) = x :: a or some other thing ? I don't see the point in universally quantifying over types which are already present in the environment; it would make better sense for me if only not yet declared types were used.

Yves Parès

8:59 a.m.

...

I don't see the point in universally quantifying over types which are already present in the environment

I think it reduces the indeterminacy you come across when you read your program ("where does this type variable come from, btw?")

...

So is there anyway to "force" the scoping of variables, so that f :: a -> a f x = x :: a becomes valid?

You mean either than compiling with ScopedTypeVariables and adding the explicit forall a. on f? I don't think. 2012/1/4 Brandon Allbery On Wed, Jan 4, 2012 at 08:41, Yves Parès wrote:

...

Would you try:

f :: a -> a f x = undefined :: a

And tell me if it works? IMO it doesn't.

...

It won't

Apparently, Yucheng says it does.

Thiago Negri

10:08 a.m.

Do not compile: f :: a -> a f x = x :: a Couldn't match type `a' with `a1' `a' is a rigid type variable bound by the type signature for f :: a -> a at C:\teste.hs:4:1 `a1' is a rigid type variable bound by an expression type signature: a1 at C:\teste.hs:4:7 In the expression: x :: a In an equation for `f': f x = x :: a Any of these compiles: f :: a -> a f x = undefined :: a f :: Num a => a -> a f x = undefined :: a f :: Int -> Int f x = undefined :: a f :: Int -> Int f x = 3 :: (Num a => a) Can someone explain case by case? Thanks, Thiago. 2012/1/4 Yves Parès :

...

...
I don't see the point in universally quantifying over types which are already present in the environment

I think it reduces the indeterminacy you come across when you read your program ("where does this type variable come from, btw?")

...
So is there anyway to "force" the scoping of variables, so that f :: a -> a f x = x :: a becomes valid?

You mean either than compiling with ScopedTypeVariables and adding the explicit forall a. on f? I don't think.

2012/1/4 Brandon Allbery

On Wed, Jan 4, 2012 at 08:41, Yves Parès wrote:

...
Would you try:

f :: a -> a

f x = undefined :: a

And tell me if it works? IMO it doesn't.

...
It won't

Apparently, Yucheng says it does.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yves Parès

10:22 a.m.

Oleg explained why those work in his last post. It's the exact same logic for each one.

...

f :: a -> a f x = x :: a

We explained that too: it's converted (alpha-converted, but I don't exactly know what 'alpha' refers to. I guess it's phase the type inferer goes through) to: f :: forall a. a -> a f x = x :: forall a1. a1 On one side, x has type a, on the other, it has type a1. Those are different polymorphic types, yet it's the same variable x hence the incompatibility. So it doesn't type-check. 2012/1/4 Thiago Negri

...

Do not compile:

f :: a -> a f x = x :: a

Couldn't match type `a' with `a1' `a' is a rigid type variable bound by the type signature for f :: a -> a at C:\teste.hs:4:1 `a1' is a rigid type variable bound by an expression type signature: a1 at C:\teste.hs:4:7 In the expression: x :: a In an equation for `f': f x = x :: a

Any of these compiles:

f :: a -> a f x = undefined :: a

f :: Num a => a -> a f x = undefined :: a

f :: Int -> Int f x = undefined :: a

f :: Int -> Int f x = 3 :: (Num a => a)

Can someone explain case by case?

Thanks, Thiago.

2012/1/4 Yves Parès :

...
...
I don't see the point in universally quantifying over types which are already present in the environment

I think it reduces the indeterminacy you come across when you read your program ("where does this type variable come from, btw?")

...
So is there anyway to "force" the scoping of variables, so that f :: a -> a f x = x :: a becomes valid?

You mean either than compiling with ScopedTypeVariables and adding the explicit forall a. on f? I don't think.

2012/1/4 Brandon Allbery

On Wed, Jan 4, 2012 at 08:41, Yves Parès wrote:

...
Would you try:

f :: a -> a

f x = undefined :: a

And tell me if it works? IMO it doesn't.

...
It won't

Apparently, Yucheng says it does.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

AUGER Cédric

12:22 p.m.

Le Wed, 4 Jan 2012 16:22:31 +0100, Yves Parès a écrit :

...

Oleg explained why those work in his last post. It's the exact same logic for each one.

...
f :: a -> a f x = x :: a

We explained that too: it's converted (alpha-converted, but I don't exactly know what 'alpha' refers to. I guess it's phase the type inferer goes through) to:

f :: forall a. a -> a f x = x :: forall a1. a1

On one side, x has type a, on the other, it has type a1. Those are different polymorphic types, yet it's the same variable x hence the incompatibility. So it doesn't type-check.

Have you ever asked what βreduction refers to? I guess that αconversion and βreduction are the two properties on the λcalculus. (γcorrection is not a λcalculus property, is just some settings for your screens.) αcorrection: λa.t = λb.t[all free occurences of a are replaced by b] if b doesn't appear in t βreduction: (λa.t)b = t[all free occurences of a are replaced by b] even if b appear in t There are also some greekletterproperty names which are common in functionnal languages: ηexpansion/contraction: λa.(f a) = f and I know that in Coq we have δ to unfold the definitions, ι for case reduction (case True of {True -> a ; False -> b} = a) and ζ for unrolling one time a fixpoint ((fix f n := match n with O => a | S n => b (f n) end) = (fun n => match n with O => a | S n => b ((fix f ... end) n) end)).

Antoine Latter

10:24 a.m.

On Wed, Jan 4, 2012 at 9:08 AM, Thiago Negri wrote:

...

Do not compile:

f :: a -> a f x = x :: a

Couldn't match type `a' with `a1' `a' is a rigid type variable bound by the type signature for f :: a -> a at C:\teste.hs:4:1 `a1' is a rigid type variable bound by an expression type signature: a1 at C:\teste.hs:4:7 In the expression: x :: a In an equation for `f': f x = x :: a

Any of these compiles:

f :: a -> a f x = undefined :: a

Re-written: f :: forall a . a -> a f x = undefined :: forall a . a Renaming variables to avoid shadowing: f :: forall a . a -> a f x = undefined :: forall b . b Which is allowed. The rest of your examples are similar - a new value is introduced with a new type that can unify with the required type. This is different from the failing case: g :: a -> a g x = x :: a Let's go through the same process. Insert foralls: g :: forall a . a -> a g x = x :: forall a . a Rename shadowed variables: g :: forall a . a -> a g x = x :: forall b . b In the function body we have declared that the value 'x' may take on any value. But that's not true! The value 'x' comes from the input to the function, which is a fixed 'a' decided by the caller. So it does not type-check. Antoine

...

f :: Num a => a -> a f x = undefined :: a

f :: Int -> Int f x = undefined :: a

f :: Int -> Int f x = 3 :: (Num a => a)

Can someone explain case by case?

Thanks, Thiago.

2012/1/4 Yves Parès :

...
...
I don't see the point in universally quantifying over types which are already present in the environment

I think it reduces the indeterminacy you come across when you read your program ("where does this type variable come from, btw?")

...
So is there anyway to "force" the scoping of variables, so that f :: a -> a f x = x :: a becomes valid?

You mean either than compiling with ScopedTypeVariables and adding the explicit forall a. on f? I don't think.

2012/1/4 Brandon Allbery

On Wed, Jan 4, 2012 at 08:41, Yves Parès wrote:

...
Would you try:

f :: a -> a

f x = undefined :: a

And tell me if it works? IMO it doesn't.

...
It won't

Apparently, Yucheng says it does.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Thiago Negri

10:46 a.m.

Got it. Thanks. :) The gotcha for me is that I was thinking as "a generic type 'a' that I may " and not in terms "if something is typed a generic 'a', then it must fit in ANY type". I think this is a common mistake, as I did read about it more than once. I.e., undefined :: a means a value that can fit in any type. (Num a => a) means a value that can fit int any type that has an instance for Num. My O.O. mind reacted to that as: Num a => a is a numeric type, it may or may not be a Int. Like type hierarchy in Java. A variable declared as "Object" does not mean that it fits in any type. It just means that you have no information about it's real type. Thiago. 2012/1/4 Antoine Latter :

...

On Wed, Jan 4, 2012 at 9:08 AM, Thiago Negri wrote:

...
Do not compile:

f :: a -> a f x = x :: a

Couldn't match type `a' with `a1' `a' is a rigid type variable bound by the type signature for f :: a -> a at C:\teste.hs:4:1 `a1' is a rigid type variable bound by an expression type signature: a1 at C:\teste.hs:4:7 In the expression: x :: a In an equation for `f': f x = x :: a

Any of these compiles:

f :: a -> a f x = undefined :: a

Re-written:

f :: forall a . a -> a f x = undefined :: forall a . a

Renaming variables to avoid shadowing:

f :: forall a . a -> a f x = undefined :: forall b . b

Which is allowed.

The rest of your examples are similar - a new value is introduced with a new type that can unify with the required type.

This is different from the failing case:

g :: a -> a g x = x :: a

Let's go through the same process.

Insert foralls:

g :: forall a . a -> a g x = x :: forall a . a

Rename shadowed variables:

g :: forall a . a -> a g x = x :: forall b . b

In the function body we have declared that the value 'x' may take on any value. But that's not true! The value 'x' comes from the input to the function, which is a fixed 'a' decided by the caller.

So it does not type-check.

Antoine

...
f :: Num a => a -> a f x = undefined :: a

f :: Int -> Int f x = undefined :: a

f :: Int -> Int f x = 3 :: (Num a => a)

Can someone explain case by case?

Thanks, Thiago.

2012/1/4 Yves Parès :

...
...
I don't see the point in universally quantifying over types which are already present in the environment

I think it reduces the indeterminacy you come across when you read your program ("where does this type variable come from, btw?")

...
So is there anyway to "force" the scoping of variables, so that f :: a -> a f x = x :: a becomes valid?

You mean either than compiling with ScopedTypeVariables and adding the explicit forall a. on f? I don't think.

2012/1/4 Brandon Allbery

On Wed, Jan 4, 2012 at 08:41, Yves Parès wrote:

...
Would you try:

f :: a -> a

f x = undefined :: a

And tell me if it works? IMO it doesn't.

...
It won't

Apparently, Yucheng says it does.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Yves Parès

8:41 a.m.

...

I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if the type of f was : f :: (forall a. a) -> (forall a. a) [1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good. Would you try: f :: a -> a f x = undefined :: a And tell me if it works? IMO it doesn't. 2012/1/4 Yucheng Zhang

...

On Wed, Jan 4, 2012 at 7:58 PM, Yves Parès wrote:

...
f :: forall a. a -> a f x = x :: forall a. a

Which is obviously wrong: when you have entered f, x has been instatiated to a specific type 'a', and then you want it to x to be of any type? That doesn't make sense.

I did not expect the type variables to be scoped.

I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem.

Yucheng Zhang

8:46 a.m.

On Wed, Jan 4, 2012 at 9:41 PM, Yves Parès wrote:

...

Would you try:

f :: a -> a f x = undefined :: a

And tell me if it works? IMO it doesn't.

It works. As I understand, in this situation we are specializing the 'undefined :: forall a. a' to a more specific dependent type.

Yves Parès

8:50 a.m.

Yes but as I understood it the type inferer was taking your type annotation for granted, and apparently in fact it re-specifies it. What you said was in reality:

...

f :: forall. a -> a f x = undefined :: forall a1. a1 And it turned it into: f :: forall. a -> a f x = undefined :: a (here, 'a' would be *scoped*)

There's something I don't get... 2012/1/4 Yucheng Zhang

...

On Wed, Jan 4, 2012 at 9:41 PM, Yves Parès wrote:

...
Would you try:

f :: a -> a f x = undefined :: a

And tell me if it works? IMO it doesn't.

It works.

As I understand, in this situation we are specializing the 'undefined :: forall a. a' to a more specific dependent type.

Brandon Allbery

8:53 a.m.

On Wed, Jan 4, 2012 at 08:41, Yves Parès wrote:

...

Would you try:

f :: a -> a f x = undefined :: a

And tell me if it works? IMO it doesn't.

It won't; a will be a new type variable unrelated to the one in the signature, in the absence of ScopedTypeVariables and an explicit forall in the signature. As I understand it, without ScopedTypeVariables the scope of type variables in the signature is exactly the signature; with ScopedTypeVariables *and* an explicit forall, the scope includes the equation. Also, I should mention that the extensions-free way to do this kind of thing is judicious use of asTypeOf. -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

AUGER Cédric

11:51 a.m.

Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès a écrit :

...

...
I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if the type of f was :

f :: (forall a. a) -> (forall a. a)

[1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good.

For the type terminology (for Haskell), notations: a Q∀ t := a universally quantified in t a Q∃ t := a existentially quantified in t a Q∀∃ t := a universally (resp. existentially) quantified in t a Q∃∀ t := a existentially (resp. universally) quantified in t Two different names are expected to denote two different type variables. A type variable is not expected to be many times quantified (else, it would be meaningless, a way to omit this hypothesis is to think of path to quantification instead of variable name; to clarify what I mean, consider the following expression: forall a. (forall a. a) -> a we cannot tell what "a is existentially quantified" means, since we have two a's; but if we rename them into forall a. (forall b. b) -> a or forall b. (forall a. a) -> b , the meaning is clear; in the following, I expect to always be in a place where it is clear.) rules: (1) ⊤ ⇒ a Q∀ forall a. t (2)b Q∀∃ t ⇒ b Q∀∃ forall a. t (3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above, since "->" is an non binding forall in type theory) (4)a Q∀∃ t ⇒ a Q∃∀ t -> u So in this context, we cannot say that 'x' is universally or existentially quantified, but that the 'type of x' is universally or existentially quantified 'in' some type (assuming that the type of x is a type variable). so: a Q∃ (forall a. a -> a) -> forall b. b -> b since (4) and "a Q∀ forall a. a -> a" due to (1) and b Q∀ (forall a. a -> a) -> forall b. b -> b since (3) and "b Q∀ forall b. b -> b" due to (1) The quick way to tell is count the number of unmatched opening parenthesis before the quantifying forall (assuming you don't put needless parenthesis) if it is even, you are universally quantified, if it is odd, you are existentially quantified. So in: f :: (forall a. a -> a) -> forall b. b -> b f id x = id x the type of 'x' (b) is universally quantified in the type of f, and the type of 'id' contains an existential quantification in the type of f (a). In: f :: forall a. (a -> a) -> a -> a f id x = id x the type of 'x' (a) is universally quantified in the type of f; there is no existential quantification. f :: forall a. (forall b. b -> b) -> a -> a f id x = id x is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b). I guess that the only difference is that when you do a "f id" in the last case, you might get an error as the program needs to know the "a" type before applying "id" (of course if there is some use later in the same function, then the type can be inferred) Hope that I didn't write wrong things, and if so that you can tell now for sure if a type is universally or existentially quantified.

Yves Parès

2:13 p.m.

...

f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

...

is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I don't get it. What is 'id' existentially quantified in? f calls id so f will decide what will be its type. In this case, because it's applied to 'x', id type will get instanciated to 'a -> a' (where a is rigid, because bound by f signature). 2012/1/4 AUGER Cédric

...

Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès a écrit :

...
...
I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if the type of f was :

f :: (forall a. a) -> (forall a. a)

[1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good.

For the type terminology (for Haskell),

notations: a Q∀ t := a universally quantified in t a Q∃ t := a existentially quantified in t a Q∀∃ t := a universally (resp. existentially) quantified in t a Q∃∀ t := a existentially (resp. universally) quantified in t

Two different names are expected to denote two different type variables. A type variable is not expected to be many times quantified (else, it would be meaningless, a way to omit this hypothesis is to think of path to quantification instead of variable name; to clarify what I mean, consider the following expression:

forall a. (forall a. a) -> a

we cannot tell what "a is existentially quantified" means, since we have two a's; but if we rename them into

forall a. (forall b. b) -> a or forall b. (forall a. a) -> b

, the meaning is clear; in the following, I expect to always be in a place where it is clear.)

rules: (1) ⊤ ⇒ a Q∀ forall a. t (2)b Q∀∃ t ⇒ b Q∀∃ forall a. t (3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above, since "->" is an non binding forall in type theory) (4)a Q∀∃ t ⇒ a Q∃∀ t -> u

So in this context, we cannot say that 'x' is universally or existentially quantified, but that the 'type of x' is universally or existentially quantified 'in' some type (assuming that the type of x is a type variable).

so:

a Q∃ (forall a. a -> a) -> forall b. b -> b since (4) and "a Q∀ forall a. a -> a" due to (1)

and

b Q∀ (forall a. a -> a) -> forall b. b -> b since (3) and "b Q∀ forall b. b -> b" due to (1)

The quick way to tell is count the number of unmatched opening parenthesis before the quantifying forall (assuming you don't put needless parenthesis) if it is even, you are universally quantified, if it is odd, you are existentially quantified.

So in:

f :: (forall a. a -> a) -> forall b. b -> b f id x = id x

the type of 'x' (b) is universally quantified in the type of f, and the type of 'id' contains an existential quantification in the type of f (a).

In:

f :: forall a. (a -> a) -> a -> a f id x = id x

the type of 'x' (a) is universally quantified in the type of f; there is no existential quantification.

f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I guess that the only difference is that when you do a "f id" in the last case, you might get an error as the program needs to know the "a" type before applying "id" (of course if there is some use later in the same function, then the type can be inferred)

Hope that I didn't write wrong things, and if so that you can tell now for sure if a type is universally or existentially quantified.

AUGER Cédric

3:44 p.m.

Le Wed, 4 Jan 2012 20:13:34 +0100, Yves Parès a écrit :

...

...
f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

...
is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I don't get it. What is 'id' existentially quantified in? f calls id so f will decide what will be its type. In this case, because it's applied to 'x', id type will get instanciated to 'a -> a' (where a is rigid, because bound by f signature).

Sorry I badly expressed it. I wanted to say that the "b" type variable in "id" is existentially quantified in the type of f. forall a. (forall b. b -> b) -> a -> a ^ existentially quantified in the overall type but locally universally quantified in the type forall b. b -> b It is the same things for data types. Consider the data type of lists: data List a = Nil | Cons a (List a) its elimination principle is: list_rec :: forall a b. b -> (a -> list a -> b -> b) -> List a -> b list_rec acc f l = case l of Nil -> acc Cons a l -> f a l (list_rec acc f l) (it is the type version of the induction principle: "∀ P. P Nil ⇒ (∀ x l, P l ⇒ P (Cons x l)) ⇒ ∀ l, P l" which by Curry-DeBruĳn-Horward gives b -> ( b -> List a -> b -> b ) -> list a -> b you can also find an "optimized" version where "l" is removed from the recursion as its information can be stored in "P l/b"; this function is exactly "foldr" ) Now if we take a look at the elimination principle, forall a b. b -> (a -> list a -> b -> b) -> List a -> b contains only universally quantified variables. Cons as a function is also universally quantified: Cons :: forall a. a -> List a -> List a Nil as a function is also universally quantified: Nil :: forall a. List a So that elimination and introduction are all universally quantified. (Nothing very surprising here!) ===================================================================== Now for the existential part: data Existential = forall b. ExistIntro b What is its elimination principle (ie. what primitive function allows us to use it for all general purpouses)? Existential types are less easy to manipulate, since in fact they require functions which takes universally quantified functions as arguments. existential_elim :: forall b. (forall a. a -> b) -> Existential -> b existential_elim f e = case e of ExistIntro x -> f x (∀ P. (∀ a. a ⇒ P (ExistIntro a)) ⇒ ∀ e. P e) Here, you can see that "a" is existentially quantified (isn't it normal for a type containing existentials)! Note also that its introduction rule: ExistIntro :: forall a. a -> Existential is also universally quantified (but with a type variable which doesn't appear in the introduced type). Which is not to mess with: data Universal = UnivIntro (forall a. a) elimination principle: univ_elim :: forall b. ((forall a. a) -> b) -> Universal -> b univ_elim f u = case u of UnivIntro poly -> f poly (∀ P. (∀ (poly:∀a.a). P (UnivIntro poly)) ⇒ ∀ u. P u) Here you can see that you don't need special syntax, and again, the elimination principle is universally quantified in both a and b. Its introduction has some existential quantification (which doesn't appear in the introduced type).

...

2012/1/4 AUGER Cédric

...
Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès a écrit :

...
...
I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if the type of f was :

f :: (forall a. a) -> (forall a. a)

[1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good.

For the type terminology (for Haskell),

notations: a Q∀ t := a universally quantified in t a Q∃ t := a existentially quantified in t a Q∀∃ t := a universally (resp. existentially) quantified in t a Q∃∀ t := a existentially (resp. universally) quantified in t

Two different names are expected to denote two different type variables. A type variable is not expected to be many times quantified (else, it would be meaningless, a way to omit this hypothesis is to think of path to quantification instead of variable name; to clarify what I mean, consider the following expression:

forall a. (forall a. a) -> a

we cannot tell what "a is existentially quantified" means, since we have two a's; but if we rename them into

forall a. (forall b. b) -> a or forall b. (forall a. a) -> b

, the meaning is clear; in the following, I expect to always be in a place where it is clear.)

rules: (1) ⊤ ⇒ a Q∀ forall a. t (2)b Q∀∃ t ⇒ b Q∀∃ forall a. t (3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above, since "->" is an non binding forall in type theory) (4)a Q∀∃ t ⇒ a Q∃∀ t -> u

So in this context, we cannot say that 'x' is universally or existentially quantified, but that the 'type of x' is universally or existentially quantified 'in' some type (assuming that the type of x is a type variable).

so:

a Q∃ (forall a. a -> a) -> forall b. b -> b since (4) and "a Q∀ forall a. a -> a" due to (1)

and

b Q∀ (forall a. a -> a) -> forall b. b -> b since (3) and "b Q∀ forall b. b -> b" due to (1)

The quick way to tell is count the number of unmatched opening parenthesis before the quantifying forall (assuming you don't put needless parenthesis) if it is even, you are universally quantified, if it is odd, you are existentially quantified.

So in:

f :: (forall a. a -> a) -> forall b. b -> b f id x = id x

the type of 'x' (b) is universally quantified in the type of f, and the type of 'id' contains an existential quantification in the type of f (a).

In:

f :: forall a. (a -> a) -> a -> a f id x = id x

the type of 'x' (a) is universally quantified in the type of f; there is no existential quantification.

f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I guess that the only difference is that when you do a "f id" in the last case, you might get an error as the program needs to know the "a" type before applying "id" (of course if there is some use later in the same function, then the type can be inferred)

Hope that I didn't write wrong things, and if so that you can tell now for sure if a type is universally or existentially quantified.

Yves Parès

5 Jan 5 Jan

6:33 a.m.

Thanks Cédric for your explanations. To sum up, that's the way I understood all this, in a bit less formal way: (Could help some, I guess) Universal quantification (forall) means that the *caller *will instanciate ("fix") the type variables, and that *callee *cannot know those types. Existential quantification (through data E = forall a. E a) means that the *callee *will fix the type variables, and that the *caller *cannot know those types. Now concerning the way existential (resp. universal) in a context becomes universal (resp. existential) in the outer context: f :: forall a. a -> a means that when you're *inside *f, 'a' will have been fixed to some type *that f cannot know*, only the outer context can. f says "I can work with any type a, so give me whatever type you want". g :: (forall a. a -> a) -> Something g f = .... means the exact opposite: 'a' is universally quantified in the signature of 'f', so it is existentially quantified in that of 'g'. So it's equivalent to: g :: exists a. (a -> a) -> Something g says "I can only work with *some* specific types 'a', but as you don't know what they will be, you can but give me something that can will work with *any *type 'a'." And so on: h :: ((forall a. a -> a) -> Something) -> SomethingElse h g = ... h can also be written as follows, am I right?: h :: forall a. ((a -> a) -> Something) -> SomethingElse And to be sure: foo :: forall a. a -> (forall b. b -> a) is equivalent to: foo :: forall a b. a -> b -> a Right? And: foo :: forall a. a -> ((forall b. b) -> a) to: foo :: forall a. exists b. a -> b -> a ?? 2012/1/4 AUGER Cédric

...

Le Wed, 4 Jan 2012 20:13:34 +0100, Yves Parès a écrit :

...
...
f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

...
is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I don't get it. What is 'id' existentially quantified in? f calls id so f will decide what will be its type. In this case, because it's applied to 'x', id type will get instanciated to 'a -> a' (where a is rigid, because bound by f signature).

Sorry I badly expressed it.

I wanted to say that the "b" type variable in "id" is existentially quantified in the type of f.

forall a. (forall b. b -> b) -> a -> a ^ existentially quantified in the overall type but locally universally quantified in the type forall b. b -> b

It is the same things for data types.

Consider the data type of lists:

data List a = Nil | Cons a (List a)

its elimination principle is:

list_rec :: forall a b. b -> (a -> list a -> b -> b) -> List a -> b list_rec acc f l = case l of Nil -> acc Cons a l -> f a l (list_rec acc f l) (it is the type version of the induction principle: "∀ P. P Nil ⇒ (∀ x l, P l ⇒ P (Cons x l)) ⇒ ∀ l, P l" which by Curry-DeBruĳn-Horward gives b -> ( b -> List a -> b -> b ) -> list a -> b you can also find an "optimized" version where "l" is removed from the recursion as its information can be stored in "P l/b"; this function is exactly "foldr" )

Now if we take a look at the elimination principle,

forall a b. b -> (a -> list a -> b -> b) -> List a -> b

contains only universally quantified variables.

Cons as a function is also universally quantified: Cons :: forall a. a -> List a -> List a

Nil as a function is also universally quantified: Nil :: forall a. List a

So that elimination and introduction are all universally quantified. (Nothing very surprising here!) =====================================================================

Now for the existential part:

data Existential = forall b. ExistIntro b

What is its elimination principle (ie. what primitive function allows us to use it for all general purpouses)?

Existential types are less easy to manipulate, since in fact they require functions which takes universally quantified functions as arguments.

existential_elim :: forall b. (forall a. a -> b) -> Existential -> b existential_elim f e = case e of ExistIntro x -> f x (∀ P. (∀ a. a ⇒ P (ExistIntro a)) ⇒ ∀ e. P e)

Here, you can see that "a" is existentially quantified (isn't it normal for a type containing existentials)!

Note also that its introduction rule: ExistIntro :: forall a. a -> Existential is also universally quantified (but with a type variable which doesn't appear in the introduced type).

Which is not to mess with:

data Universal = UnivIntro (forall a. a)

elimination principle: univ_elim :: forall b. ((forall a. a) -> b) -> Universal -> b univ_elim f u = case u of UnivIntro poly -> f poly (∀ P. (∀ (poly:∀a.a). P (UnivIntro poly)) ⇒ ∀ u. P u)

Here you can see that you don't need special syntax, and again, the elimination principle is universally quantified in both a and b. Its introduction has some existential quantification (which doesn't appear in the introduced type).

...
2012/1/4 AUGER Cédric

...
Le Wed, 4 Jan 2012 14:41:21 +0100, Yves Parès a écrit :

...
...
I expected the type of 'x' to be universally quantified, and thus can be unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1] x would be universally quantified if the type of f was :

f :: (forall a. a) -> (forall a. a)

[1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good.

For the type terminology (for Haskell),

notations: a Q∀ t := a universally quantified in t a Q∃ t := a existentially quantified in t a Q∀∃ t := a universally (resp. existentially) quantified in t a Q∃∀ t := a existentially (resp. universally) quantified in t

Two different names are expected to denote two different type variables. A type variable is not expected to be many times quantified (else, it would be meaningless, a way to omit this hypothesis is to think of path to quantification instead of variable name; to clarify what I mean, consider the following expression:

forall a. (forall a. a) -> a

we cannot tell what "a is existentially quantified" means, since we have two a's; but if we rename them into

forall a. (forall b. b) -> a or forall b. (forall a. a) -> b

, the meaning is clear; in the following, I expect to always be in a place where it is clear.)

rules: (1) ⊤ ⇒ a Q∀ forall a. t (2)b Q∀∃ t ⇒ b Q∀∃ forall a. t (3)a Q∀∃ u ⇒ a Q∀∃ t -> u (in fact it is the same rule as above, since "->" is an non binding forall in type theory) (4)a Q∀∃ t ⇒ a Q∃∀ t -> u

So in this context, we cannot say that 'x' is universally or existentially quantified, but that the 'type of x' is universally or existentially quantified 'in' some type (assuming that the type of x is a type variable).

so:

a Q∃ (forall a. a -> a) -> forall b. b -> b since (4) and "a Q∀ forall a. a -> a" due to (1)

and

b Q∀ (forall a. a -> a) -> forall b. b -> b since (3) and "b Q∀ forall b. b -> b" due to (1)

The quick way to tell is count the number of unmatched opening parenthesis before the quantifying forall (assuming you don't put needless parenthesis) if it is even, you are universally quantified, if it is odd, you are existentially quantified.

So in:

f :: (forall a. a -> a) -> forall b. b -> b f id x = id x

the type of 'x' (b) is universally quantified in the type of f, and the type of 'id' contains an existential quantification in the type of f (a).

In:

f :: forall a. (a -> a) -> a -> a f id x = id x

the type of 'x' (a) is universally quantified in the type of f; there is no existential quantification.

f :: forall a. (forall b. b -> b) -> a -> a f id x = id x

is very similar to the first case, x is still universally quantified (a) and there is an existential quantification in id (b).

I guess that the only difference is that when you do a "f id" in the last case, you might get an error as the program needs to know the "a" type before applying "id" (of course if there is some use later in the same function, then the type can be inferred)

Hope that I didn't write wrong things, and if so that you can tell now for sure if a type is universally or existentially quantified.

4887

Age (days ago)

4889

Last active (days ago)

List overview

Download

45 comments

8 participants

participants (8)

Antoine Latter
AUGER Cédric
Bardur Arantsson
Brandon Allbery
Brent Yorgey
Thiago Negri
Yucheng Zhang
Yves Parès