[Haskell-cafe] phantom types
Hi, I am currently reading documentation on Generalized Algebraic Data Types: http://en.wikibooks.org/wiki/Haskell/GADT I have a question concerning this page. Let us consider the following code proposed in the page: -- -- Phantom type variable a (does not appear in any Expr: it is just a -- dummy variable). data Expr a = I Int | B Bool | Add (Expr a) (Expr a) | Mul (Expr a) (Expr a) | Eq (Expr a) (Expr a) deriving (Show) -- Smart constructors add :: Expr Int -> Expr Int -> Expr Int add = Add i :: Int -> Expr Int i = I b :: Bool -> Expr Bool b = B eval :: Expr a -> a eval (I n) = n -- I obtain the following error: Phantom.hs:27:14: Couldn't match type `a' with `Int' `a' is a rigid type variable bound by the type signature for eval :: Expr a -> a at Phantom.hs:27:1 In the expression: n In an equation for `eval': eval (I n) = n The wiki page explains: """ But alas, this does not work: how would the compiler know that encountering the constructor I means that a = Int? """ I don't understand. When we write "eval (I n) = n", as I is a constructor which takes an Int as argument, we are able to deduce that the type of n is Int; so the type of eval should be in this case "Expr Int -> Int". What do I miss? Thanks, TP___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] phantom types
> Hi, > > I am currently reading documentation on Generalized Algebraic Data Types: > > http://en.wikibooks.org/wiki/Haskell/GADT > > I have a question concerning this page. Let us consider the following code > proposed in the page: > > -- > -- Phantom type variable a (does not appear in any Expr: it is just a > -- dummy variable). > data Expr a = I Int > | B Bool > | Add (Expr a) (Expr a) > | Mul (Expr a) (Expr a) > | Eq (Expr a) (Expr a) > deriving (Show) > > -- Smart constructors > add :: Expr Int -> Expr Int -> Expr Int > add = Add > > i :: Int -> Expr Int > i = I > > b :: Bool -> Expr Bool > b = B > > eval :: Expr a -> a > eval (I n) = n > -- > > I obtain the following error: > > Phantom.hs:27:14: > Couldn't match type `a' with `Int' > `a' is a rigid type variable bound by > the type signature for eval :: Expr a -> a at Phantom.hs:27:1 > In the expression: n > In an equation for `eval': eval (I n) = n > > The wiki page explains: > > """ > But alas, this does not work: how would the compiler know that encountering > the constructor I means that a = Int? > """ > > I don't understand. When we write "eval (I n) = n", as I is a constructor > which takes an Int as argument, we are able to deduce that the type of n is > Int; so the type of eval should be in this case "Expr Int -> Int". > What do I miss? Since the example uses phantom types, the type of n is not actually related to the type of (I n). It is perfectly possible to have, for example, a value of type Expr String created by the I constructor: *Main> let expr = I 5 :: Expr String *Main> expr I 5 *Main> :t expr expr :: Expr String So if we define eval the way it is defined in the example, the compiler cannot infer that the type of (I n) is Expr Int, even though it knows that n's type is Int. We could prevent the creation of values with the wrong types by only exporting the smart constructors, but that is no help for the type system. Declaring eval as Expr Int -> Int would make the code compile, but since eval should presumably include patterns for other types, such as eval (B b) = b which would have to be of type Expr Bool -> Bool, we cannot do that. I hope I did not misunderstand your question and this helps. Cheers, Florian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] phantom types
First, thanks for your answer. On Friday, August 17, 2012 15:31:32 you wrote: > So if we define eval the way it is defined in the example, the > compiler cannot infer that the type of (I n) is Expr Int, even though > it knows that n's type is Int. I think that my problem came from the fact that I have misunderstood type variables. We have seen that the function eval: eval :: Expr a -> a eval (I n) = n yields a compilation error: """ Phantom.hs:37:14: Couldn't match type `a' with `Int' `a' is a rigid type variable bound by the type signature for eval :: Expr a -> a """ A somewhat similar error is found at http://stackoverflow.com/questions/4629883/rigid-type-variable-error test :: Show s => s test = "asdasd" yields a compilation error: """ Could not deduce (s ~ [Char]) from the context (Show s) bound by the type signature for test :: Show s => s at Phantom.hs:40:1-15 `s' is a rigid type variable bound by the type signature for test :: Show s => s """ Both errors contain the expression "rigid type variable". The explanation in the Stack Overflow page made me understand my error: test :: Show s => s means "for any type s which is an instance of Show, test is a value of that type s". Something like test :: Num a => a; test = 42 works because 42 can be a value of type Int or Integer or Float or anything else that is an instance of Num. However "asdasd" can't be an Int or anything else that is an instance of Show - it can only ever be a String. As a consequence it does not match the type Show s => s. The compiler does not say: «s is of type String because the return type of test is a String». Identically, in our case, «eval :: Expr a -> a» means «for any type a, eval takes a value of type «Expr a» as input, and outputs a value of type a». Analogously to the above case, the compiler does not say «a is of type Int, because n is of type Int». The problem here is that (I n) does not allow to know the type of a. It may be of type Expr String as you have shown: *Main> let expr = I 5 :: Expr String *Main> expr I 5 *Main> :t expr expr :: Expr String So we may have anything for «a» in «Expr a» input type of eval. These multiplicity of values for «a» cannot match the output type of the equation «eval (I n) = n» which is an Int. Thus we get an error. Am I correct? Thanks, TP ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] phantom types
On 8/17/12 5:35 AM, TP wrote: Hi, I am currently reading documentation on Generalized Algebraic Data Types: http://en.wikibooks.org/wiki/Haskell/GADT I have a question concerning this page. Let us consider the following code proposed in the page: -- -- Phantom type variable a (does not appear in any Expr: it is just a -- dummy variable). data Expr a = I Int | B Bool | Add (Expr a) (Expr a) | Mul (Expr a) (Expr a) | Eq (Expr a) (Expr a) deriving (Show) [...] I don't understand. When we write "eval (I n) = n", as I is a constructor which takes an Int as argument, we are able to deduce that the type of n is Int; so the type of eval should be in this case "Expr Int -> Int". What do I miss? Perhaps it'd help to rewrite the above ADT using GADT syntax (but note that its the exact same data type): data Expr :: * -> * where I :: Int -> Expr a B :: Bool -> Expr a Add :: Expr a -> Expr a -> Expr a Mul :: Expr a -> Expr a -> Expr a Eq :: Expr a -> Expr a -> Expr a So, when looking at the pattern (I n), since I :: Int -> Expr a we know that n :: Int and that (I n) :: Expr a. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] phantom types
On Aug 19, 2012, at 5:29 , wren ng thornton wrote:
> On 8/17/12 5:35 AM, TP wrote:
>> Hi,
>>
>> I am currently reading documentation on Generalized Algebraic Data Types:
>>
>> http://en.wikibooks.org/wiki/Haskell/GADT
>>
>> I have a question concerning this page. Let us consider the following code
>> proposed in the page:
>>
>> --
>> -- Phantom type variable a (does not appear in any Expr: it is just a
>> -- dummy variable).
>> data Expr a = I Int
>> | B Bool
>> | Add (Expr a) (Expr a)
>> | Mul (Expr a) (Expr a)
>> | Eq (Expr a) (Expr a)
>> deriving (Show)
>> [...]
>> I don't understand. When we write "eval (I n) = n", as I is a constructor
>> which takes an Int as argument, we are able to deduce that the type of n is
>> Int; so the type of eval should be in this case "Expr Int -> Int".
>> What do I miss?
>
> Perhaps it'd help to rewrite the above ADT using GADT syntax (but note that
> its the exact same data type):
>
>data Expr :: * -> * where
>I :: Int -> Expr a
>B :: Bool -> Expr a
>Add :: Expr a -> Expr a -> Expr a
>Mul :: Expr a -> Expr a -> Expr a
>Eq :: Expr a -> Expr a -> Expr a
But if you use the real power of GADT's you would write:
{-# LANGUAGE KindSignatures, GADTs #-}
data Expr :: * -> * where
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Val :: a-> Expr a
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr Int
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
eval :: Expr a -> a
eval (I i) = i
eval (B b) = b
eval (Val v) = v
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq e1 e2) = eval e1 == eval e2
>
Note that the I and B cases are actually superfluous, and are covered by the
val case. This has all nothing to do with phnatom types, but with a proper
understanding of the GADT concept.
Doaitse
> So, when looking at the pattern (I n), since I :: Int -> Expr a we know that
> n :: Int and that (I n) :: Expr a.
>
> --
> Live well,
> ~wren
>
> ___
> 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
[Haskell-cafe] phantom types for inheritance between types
there are packages which use phantom types to express inheritance (subtype) relations. unfortunately i cannot find a simple example and seem to misunderstand something. can somebody help with the following simple example? i have a most general type Dated, a subtype Note and a subsubtype Task. i have only instances for Note and Task, but operations for tasks and dated. my primary question is: why should i have the contexts in the classes (the code compiles without them)? they do not say more than what is already expressed in the instance declarations. i do also not think that i have used phantom types properly (eg. gtk2hs uses phantom types differently). what would be the proper solution? would it work for cases with multiple inheritance? thank you! andrew class CDated a class CDated a => CNotes a class CNotes a => CTasks a instance CDated Task instance CDated Note instance CNotes Note instance CNotes Task instance CTasks Task class Dated n where datedop :: n -> n class Notes1 n where noteop :: n -> n class Tasks1 n where taskop :: n -> n data Note = Note Int data Task = Task Int instance CTasks x => Tasks1 x where taskop n = n instance CDated x => Dated x where datedop n = n t:: Task = Task 1 n :: Note = Note 1 tt = taskop t -- nt = taskop n -- compiler error -- as expected! tx = datedop t nx = datedop n ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
