Motivation

• Use types to express invariants of our code
• Ensure correct use of libraries and APIs
• Detect errors at compile-time instead of run-time
• Encode domain-specific knowledge

Encoding invariants in types

Dependent types

• Active area for research languages
• Examples: Agda, Idris

Phantom types and GADTs

• Expressible in many modern languages (varying degrees)
• Examples: Haskell, OCaml, F#, Scala, C++, Java, Swift, Rust

Phantom types

Example: money

• Represent amounts of money in different currencies (e.g. US dollars, Euro)
• Track currencies using types
  • e.g. avoid adding Dollars to Euros

First attempt

newtype USD = USD Integer
    deriving (Eq, Ord, Show, Num)
            
newtype EUR = EUR Integer
    deriving (Eq, Ord, Show, Num)   

The different types avoid mixing currencies:

> 100 :: USD + 50 :: EUR
-- Couldn't match expected type
-- ‘EUR’ with actual type ‘USD’

Limitations

No way to write a generic function, e.g. to apply an interest rate:

interest :: Float -> USD -> USD
interest :: Float -> EUR -> EUR

Second attempt

A money type with a phantom parameter (currency):

newtype Money curr = Money Integer
           -- ^ phantom parameter 

data USD   -- phantom types for currencies
data EUR
...

instance Show (Money USD) ...
instance Show (Money EUR) ...

Phantom currencies

• The currency types have no data constructors
• They are only used at compile-time to tag money
• The compiler checks currencies at compile time:

  > 100 :: Money USD + 50 :: Money EUR
  --  Couldn't match expected type ‘EUR’ 
  --  with actual type ‘USD’

• No run-time cost: money amounts are just integers

Generic currency functions

interest :: Float -> Money curr -> Money curr
interest rate (Money amount) 
   = Money (round (rate*fromIntegral amount))

> rate 0.1 (100 :: Money USD)
USD 10 

> rate (1/3) (100 :: Money EUR)
EUR 33

Second example: ST monad

newSTRef :: a -> ST s (STRef s a)
                --  ^--------^ phantom param
                
runST :: (forall s. ST s a) -> a
            --   ^----- prevents escape

The s parameter ensures safe use of the library: references cannot escape the ST computation.

GADTs

Algebraic data types

• Algebraic data types are sums of products
• Every alternative declares a constructor with one or more arguments
• All alternatives have the same result type

data Bool = True | False

data Maybe a = Nothing | Just a

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

Using GADT syntax

{-# LANGUAGE GADTs #-}

data Bool where
    True :: Bool
    False :: Bool
    
data Maybe a where
    Nothing :: Maybe a
    Just :: a -> Maybe a
    
data List a where
    Nil :: List a 
    Cons :: a -> List a -> List a

Generalized Algebraic DataTypes

• GADTs allow specifying the type of each constructor
• This can be used to encode information in types
• Pattern matching refines type information

Example: non-empty lists

A type that distinguished empty from non-empty lists:

• List Empty is always empty
• List NonEmpty is always non-empty

data Empty     -- phantom types
data NonEmpty

data List t a where
   Nil :: List Empty a 
   Cons :: a -> List t a -> List NonEmpty a

Examples

Nil          :: List Empty a
Cons 'A' Nil :: List NonEmpty Char
Cons 1 (Cons 2 Nil) :: List NonEmpty Int

Non-empty lists (cont.)

We can now define a safe head function:

safeHead :: List NonEmpty a -> a
safeHead (Cons x xs) = x

We get a type error if we apply to the empty list:

> safeHead Nil
 -- Couldn't match type ‘Empty’ with ‘NonEmpty’

Also a type error to add an equation safeHead Nil = ....

Sized lists

A type for lists of a given length (also know as vectors):

List Z           -- length 0
List (S Z)       -- length 1
List (S (S Z))   -- length 2
...              -- etc.

Sized lists (cont.)

data Z    -- type-level Peano naturals
data S n  -- i.e., Z, S Z, S (S Z), ...

data List n a where
  Nil :: List Z a
  Cons :: a -> List n a -> List (S n) a

• Nil has length zero
• The length of the result list of Cons is one more than the length of argument

Programming with sizes

We can now define both safe head and safe tail.

safeHead :: List (S n) a -> a
safeHead (Cons x xs) = x

safeTail :: List (S n) a -> List n a
safeTail (Cons x xs) = xs

• The types requires that the arguments is non-empty
• The result of safeTail has length one less than the argument
• Both functions are total: no run-time exceptions!

Size relations

zip :: List n a -> List n b -> List n (a,b)
zip Nil Nil = Nil
zip (Cons x xs) (Cons y ys) 
                   = Cons (a,b) (zip xs ys)

• Both arguments must have the same length
• Hence: there are no missing cases in the above definition
• And the result list will preserve the length

Size relations (cont.)

map :: (a -> b) -> List n a -> List n b
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

• The type encode the preservion of list length
• A wrong definition would be rejected, e.g.

map f (Cons x xs) = map f xs
-- type error: Cannot deduce n1 ~ S n1 ...

Beyond equality

• What if we need to express relations other than equality?
• E.g. appending two lists should add their lengths
• For that we need computation at the type level

append :: List n a -> List m a 
                   -> List (Add n m) a 
 -- Add n m: addition of type-level naturals

Appending lists

{-# LANGUAGE TypeFamilies #-}

append :: List n a -> List m a
                   -> List (Add n m) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

-- a type-level function for addition
type family Add n m
type instance Add Z y = y
type instance Add (S x) y = S (Add x y)

Appending lists: example

>  append (Cons 1 Nil) (Cons 2 Nil)
Cons 1 (Cons 2 Nil) 
> :t append (Cons 1 Nil) (Cons 2 Nil)
List (S (S Z)) Int

(show interactive example.)

Appending lists (version 2)

We can make the syntax nicer with type level operators:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

append :: List n a -> List m a -> List (n+m) a
...
-- addition using type operators
type family n + m
type instance Z + y = y
type instance (S x) + y = S (x+y)

Towards dependent types?

• Dependent type systems allow types to depend on values
• Theorical basis for interactive theorem provers: Coq
• Also for new research languages: Agda, Idris

Will the next Haskell be a fully-dependently typed language?