Newbie question (again!) about phantom types
I’m having difficulty to understand what phantom types are good for. Is this just for improving runtime performance? I read the wiki, and it says "this is useful if you want to increase the type-safety of your code", but the code below does not give a compiler error for the function test1, I get a runtime error, just like test2. Thanks, Peter -- CODE -- -- With phantom types data T1 a = TI1 Int | TS1 String deriving Show foo1 :: T1 String -> T1 String -> T1 String foo1 (TS1 x) (TS1 y) = TS1 (x++y) test1 = foo1 (TI1 1) (TI1 2) -- Shouldn't this give a compiler error instead of a runtime error? -- Without phantom types data T2 = TI2 Int | TS2 String deriving Show foo2 :: T2 -> T2 -> T2 foo2 (TS2 x) (TS2 y) = TS2 (x++y) test2 = foo2 (TI2 1) (TI2 2) No virus found in this outgoing message. Checked by AVG Free Edition. Version: 7.5.476 / Virus Database: 269.11.8/941 - Release Date: 07/08/2007 16:06
peterv wrote:
I’m having difficulty to understand what phantom types are good for.
I read the wiki, and it says "this is useful if you want to increase the type-safety of your code", but the code below does not give a compiler error for the function test1, I get a runtime error, just like test2.
-- With phantom types data T1 a = TI1 Int | TS1 String deriving Show
foo1 :: T1 String -> T1 String -> T1 String foo1 (TS1 x) (TS1 y) = TS1 (x++y)
test1 = foo1 (TI1 1) (TI1 2) -- Shouldn't this give a compiler error instead -- of a runtime error?
You have to manually instantiate the phantom type variable. In your code, the type of TI1 1 is just T1 a for an unrestricted type variable a. This unifies fine with the expected argument type of foo1, wich is T1 String, by setting a = String. Consider this variant of your code: -- the type of things wich can hold numbers or text -- what exactly they hold is encoded dynamically by the -- constructor used and statically by the phantom type data Container a = NumberContainer Int | TextContainer String data Number = Number data Text = Text -- approbiate smart constructors. only use these for creation -- of containers, never use the real constructors. number :: Int -> Container Number number x = NumberContainer x text :: String -> Container Text text x = TextContainer x -- a function wich works only on containers holding text foo :: Container Text -> Container Text -> Container Text foo (TextContainer a) (TextContainer b) = text (a ++ b) -- testing test1 = text "hello " `foo` text "world" -- works test2 = number 13 `foo` number 19 -- static error This works fine when you can decide statically how to instantiate the phantom type variable (by using the approbiate smart constructor). If you can't (because you read data from same external source, for example), you can restrict the position of dynamic failures to a well-defined point in program execution by defining asText :: Container a -> Maybe (Container Text) asText (TextContainer x) = Just $ text x asText _ = Nothing asNumber :: Container a -> Maybe (Container Number) asNumber (NumberContainer x) = Just $ number x asNumber _ = Nothing Using these functions, you can lift a dynamic typecheck (is it the right constructor?) to a static typecheck (has it the right phantom type?). So you can for example check user input once for having the correct form and then enter the statically typesafe part of your program, where you don't have to worry about people entering numbers instead of text, because you statically know that at this point in program execution, the dynamic typecheck already suceeded. Tillmann
Im having difficulty to understand what phantom types are good for. Is this just for improving runtime performance?
No. As the wiki says, you can use them to add static guarantees.
I read the wiki, and it says "this is useful if you want to increase the type-safety of your code", but the code below does not give a compiler error for the function test1, I get a runtime error, just like test2.
It seems you're mixing up GADT's and phantom types.
-- CODE -- -- With phantom types data T1 a = TI1 Int | TS1 String deriving Show
Here, the 'a' is an extra type parameter, which has no manifestation on the value level. Note the type of the constructors: TI1 :: Int -> T1 a TS1 :: String -> T1 a In particular, the 'a' is not related to the 'Int' or 'String' arguments.
foo1 :: T1 String -> T1 String -> T1 String foo1 (TS1 x) (TS1 y) = TS1 (x++y)
test1 = foo1 (TI1 1) (TI1 2) -- Shouldn't this give a compiler error instead of a runtime error?
'TI1 1' has type 'T1 a', so this unifies with 'T1 String' (the type of the argument of 'foo1'. The type parameter 'a' can still be useful, but you have to use an explicit type signature to constrain the type 'a': ti1 :: Int -> T1 Int ti1 x = TI1 x Now, 'ti1' will create values with the restricted type 'T1 Int', that you can't use as arguments for your 'foo1'. GADTs are perhaps more useful for what you seem to want. Try something like this: data T1 :: * -> * where -- T1 has one type parameter TI1 :: Int -> T1 Int TS1 :: String -> T1 String Now, the type systems guarantees that all values of the form 'TI1 x' have type 'T1 Int'. Greetings, Arie
Thanks, that is a much clearer explanation than http://en.wikibooks.org/wiki/Haskell/Phantom_types Peter -----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Arie Peterson Sent: Wednesday, August 08, 2007 5:59 PM To: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] Newbie question (again!) about phantom types
I'm having difficulty to understand what phantom types are good for. Is this just for improving runtime performance?
No. As the wiki says, you can use them to add static guarantees.
I read the wiki, and it says "this is useful if you want to increase the type-safety of your code", but the code below does not give a compiler error for the function test1, I get a runtime error, just like test2.
It seems you're mixing up GADT's and phantom types.
-- CODE -- -- With phantom types data T1 a = TI1 Int | TS1 String deriving Show
Here, the 'a' is an extra type parameter, which has no manifestation on the value level. Note the type of the constructors: TI1 :: Int -> T1 a TS1 :: String -> T1 a In particular, the 'a' is not related to the 'Int' or 'String' arguments.
foo1 :: T1 String -> T1 String -> T1 String foo1 (TS1 x) (TS1 y) = TS1 (x++y)
test1 = foo1 (TI1 1) (TI1 2) -- Shouldn't this give a compiler error instead of a runtime error?
'TI1 1' has type 'T1 a', so this unifies with 'T1 String' (the type of the argument of 'foo1'. The type parameter 'a' can still be useful, but you have to use an explicit type signature to constrain the type 'a': ti1 :: Int -> T1 Int ti1 x = TI1 x Now, 'ti1' will create values with the restricted type 'T1 Int', that you can't use as arguments for your 'foo1'. GADTs are perhaps more useful for what you seem to want. Try something like this: data T1 :: * -> * where -- T1 has one type parameter TI1 :: Int -> T1 Int TS1 :: String -> T1 String Now, the type systems guarantees that all values of the form 'TI1 x' have type 'T1 Int'. Greetings, Arie _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Aug 8, 2007, at 11:16 AM, peterv wrote:
I’m having difficulty to understand what phantom types are good for. Is this just for improving runtime performance?
I found phantom types to be useful in the implementation of bit-wise set operations. You can find the code Edison: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/ EdisonCore-1.2.1 in the Data.Edison.Coll.EnumSet module. David F. Place mailto:d@vidplace.com
participants (4)
-
Arie Peterson -
David F. Place -
peterv -
Tillmann Rendel