Haskell/Phantom types

From Wikibooks, the open-content textbooks collection

Jump to: navigation, search
Phantom types (Solutions)

Contents

Fun with Types

Polymorphism basics 25%.png
Existentially quantified types 25%.png
Advanced type classes 25%.png
Phantom types 25%.png
Generalised algebraic data-types (GADT) 25%.png
Datatype algebra 00%.png
Type constructors & Kinds 00%.png

Phantom types are a way to embed a language with a stronger type system than Haskell's. FIXME: that's about all I know, and it's probably wrong. :) I'm yet to be convinced of PT's usefulness, I'm not sure they should have such a prominent position. DavidHouse 17:42, 1 July 2006 (UTC)

[edit] Phantom types

An ordinary type

data T = TI Int | TS String

plus :: T -> T -> T
concat :: T -> T -> T

its phantom type version

data T a = TI Int | TS String

Nothing's changed - just a new argument a that we don't touch. But magic!

plus :: T Int -> T Int -> T Int
concat :: T String -> T String -> T String

Now we can enforce a little bit more!

This is useful if you want to increase the type-safety of your code, but not impose additional runtime overhead:

-- Peano numbers at the type level.
data Zero = Zero
data Succ a = Succ a
-- Example: 3 can be modeled as the type
-- Succ (Succ (Succ Zero)))

data Vector n a = Vector [a] deriving (Eq, Show)

vector2d :: Vector (Succ (Succ Zero)) Int
vector2d = Vector [1,2]

vector3d :: Vector (Succ (Succ (Succ Zero))) Int
vector3d = Vector [1,2,3]

-- vector2d == vector3d raises a type error
-- at compile-time, while vector2d == Vector [2,3] works.