# A bit about what I do

Research (UPB/ACS)

• Improving the security of software systems

• In general, system software

• In particular, operating systems

# A bit about what I do

Development (VirtualMetrix)

• VMXL4, a "provably secure" microkernel/hypervisor

• Virtualization for mobile phones

# A bit about what I do

Teaching assistant (UPB/ACS) for the following courses:

• Operating System Security

• Pure, lazy
• Strongly typed, statically-typed

Haskell's type system has the following particularities:

• Algebraic data types
• Parametric polymorphism

# Algebraic data types

• Either a primitive type

• Or a sum of types

• Or a product of types

# Example 1: primitive types

``````3 :: Int
120894192912541294198294982 :: Integer
3.14 :: Float
'a' :: Char
"The cake is a lie" :: String
True :: Bool``````
• `::` is similar to set membership ( ∈ )
• Intuition: types are (a generalization of) sets

# Example 2: sum types

• Problem: encode an enumeration of fruits
• Suppose we wish to have exactly four types of fruit
• Apples
• Pears
• Oranges
• Tomatoes

# Example 2 in C

``````typedef enum {
Apples = 1,
Pears = 2,
Oranges = 3,
Tomatoes = 4
} fruit_e;``````

Now we can say:

``fruit_e fr = Tomatoes;``

# Example 2 in C

``````typedef enum {
Apples = 1,
Pears = 2,
Oranges = 3,
Tomatoes = 4
} fruit_e;``````

But we can also say:

``fruit_e fr = 5;``

``````data Fruit =
Apples
| Pears
| Oranges
| Tomatoes``````
• `Fruit` is the type's name
• `|` is the sum type-level operator
• `Apples`, `Pears`, `Oranges`, `Tomatoes` are possible values
• More generally, constructors

``````data Fruit =
Apples
| Pears
| Oranges
| Tomatoes``````
``````> :t Apples
Apples :: Fruit
> 5 :: Fruit

<interactive>
No instance for (Num Fruit) ..``````

``````data Fruit =
Apples
| Pears
| Oranges
| Tomatoes``````
• Note: we select one of the values in `Fruit`
• `|` is in general similar to `union`s
• Intuition: `|` is the logical equivalent of or

# Example 3: product types

• Problem: encode "a bucket of fruit"
• A bucket of fruit consists of:
• A type of fruit
• The quantity of fruit in the bucket

# Example 3

Possible approach: use built-in pairs

``````> :t (,)
(,) :: a -> b -> (a, b)
> (,) Pears 2 :: (Fruit, Int)
(Pears,2)
> (Pears, 2) -- sugar
(Pears,2)``````
• `(,)` defines pairs of values
• Note: small letters denote type variables
• Parametric polymorphism

# Example 3

``data Bucket = MkBucket Fruit Int``
• `Bucket` is the type's name
• `MkBucket` is the constructor
``````> :t MkBucket
MkBucket :: Fruit -> Int -> Bucket``````

# Example 3

• It may be useful to generalize
• In this case, `Fruit` is too particular
``data Bucket a = MkBucket a Int``

# Example 3

• We can implicitly define field selectors
• ... by using record notation
``````data Bucket a = MkBucket
{ bucketObject  :: a
, bucketQty     :: Int
}``````
``````> let myBucket = MkBucket Apples 10
> bucketQty myBucket
10``````

# Example 3

• We can implicitly define field selectors
• ... by using record notation
``````data Bucket a = MkBucket
{ bucketObject  :: a
, bucketQty     :: Int
}``````
• Type fields are similar to `struct`s
• Intuition: tuples are the logical equivalent of and

# Example 4: MultiBuckets

• What if we want to hold more than one type of fruit in a bucket?
``> MkBucket (Pears, Apples) 50``
• ... but we can't distinguish between types of fruits
• Idea: `MultiBucket`s as lists of `Bucket`s

# Example 4

``type MultiBucket a = [Bucket a]``
• `type` is similar to C's `typedef`
• Type synonyms
• Note: synonyms are not subjected to type checking
• E.g. `MultiBucket a` and `[Bucket a]` are the same type

# Example 4

``type MultiBucket a = [Bucket a]``

Extracting all the `Apple`s from a MultiBucket

``````> let mb = [MkBucket Apples 20,
MkBucket Pears 30]
filter (\ b -> bucketObject b == Apples ) mb
MkBucket {bucketObject = Apples, bucketQty = 20}``````

# Example 4

``type MultiBucket a = [Bucket a]``

What if there are no apples in the MultiBucket?

``````> let mb = [MkBucket Pears 30]
filter (\ b -> bucketObject b == Apples ) mb

# Example 5: representing failure

``data Maybe a = Nothing | Just a``
• `Nothing` is similar to `void`
• `Just` is a 1-tuple that wraps values
• Intuition: return `Nothing` on failure

# Example 5

``````getBucket :: Fruit -> MultiBucket Fruit
-> Maybe (Bucket Fruit)
getBucket obj mb = case filter isEqual mb of
[]      -> Nothing
(x : _) -> Just x
where isEqual x = bucketObject x == obj``````
• Note: `case` performs pattern matching on values
• Note: `[]` is the empty list; `x : list` is a non-empty list

# Example 5

``````> let mb = [MkBucket Pears 30]
> getBucket Apples mb
Nothing
> getBucket Pears mb
Just (MkBucket
{bucketObject = Pears, bucketQty = 30})``````

# Example 5

We can make `getBucket` polymorphic:

``````getBucket :: Eq a => a -> MultiBucket a
-> Maybe (Bucket a)``````
• Implementation stays the same
• `Eq a`: constraint imposed on `a` due to `(==)`

# Example 5

``````> :t (==)
(==) :: Eq a => a -> a -> Bool``````
• `deriving` tries to automatically implement `(==)` for ADTs
• `Eq a` is a type class constraint
• `Eq a`  ≡  "all types `a` that implement `(==)`"

# Example 6: seL4 kernel objects

`````` data KernelObject
= KOEndpoint  Endpoint
| KOAEndpoint AsyncEndpoint
| KOKernelData
| KOUserData
| KOTCB       TCB
| KOCTE       CTE
| KOArch      ArchKernelObject``````

# Example 6

``````data TCB = Thread {
tcbCTable :: CTE,
tcbVTable :: CTE,
tcbCaller :: CTE,
tcbIPCBufferFrame :: CTE,
tcbDomain :: Domain,
..
tcbFaultHandler :: CPtr,
tcbIPCBuffer :: VPtr,
tcbContext :: UserContext }
deriving Show``````

# Example 7: natural numbers

`Bucket`s can have non-sensical values:

``````> :t MkBucket Apples (-2)
MkBucket Apples (-2) :: Bucket Fruit``````

# Example 7

Possible approach: smart constructors

``newtype Nat1 = Nat1 { fromNat1 :: Int }``
• `newtype` is like `data`, only
• It has exactly one constructor
• ... and exactly one field
• Additionally, it's erased at compile-time

# Example 7

Possible approach: smart constructors

``````mkNat :: Int -> Nat1
mkNat n = if n < 0
then error "Only positive numbers are permitted"
else Nat1 n``````
• `mkNat` checks for positive numbers at run-time
• It provides some compile-time guarantees
• All type conversions are explicit
• Signedness is (a weak) invariant under `Nat1`

# Example 8: more naturals

Possible approach: Peano naturals

``data Nat2 = Z | S Nat2``
``````> :t Z -- 0
Z :: Nat2
> :t S \$ S \$ S Z -- 3
S \$ S \$ S Z :: Nat2``````

# Example 8

Possible approach: Peano naturals

``data Nat2 = Z | S Nat2``
• Very clunky and inefficient
• Works well for small enough numbers

# Example 9: even more naturals

Possible approach: type-level numbers

``````data Z
data S n``````
• `Z` and `S n` are types encoding numbers!
• Note: `Z` and `S n` lack constructors

# Digression: kinds

• Types also have types
• They are called kinds
``````> :k Z
Z :: *
> :k S
S :: * -> *
> :k (S (S Z))
(S (S Z)) :: *``````
• Well-formed typed expressions have the kind `*`

# Digression: type classes

``````class MyClass a where
myMethod :: a -> Int

instance MyClass Int where
myMethod = (+ 1) . fromIntegral``````
``````> myMethod (42 :: Int)
42``````

# Example 9

First we define cardinalities on type-level naturals

``````class Card n where

instance Card Z where
instance (Card n) => Card (S n) where``````
• Note: computations are done purely at type-level
• type class and instances have no methods

# Example 9

Next, we define a class for bound checking

``````class (Card n) => InBounds n where

instance InBounds (S Z) where
instance InBounds (S (S Z)) where
instance InBounds (S (S (S Z))) where``````

# Example 9

Finally, we define a concrete type and a smart constructor

``````data MaxThree n = MaxThree
deriving Show

maxthree :: InBounds n => n -> MaxThree n
maxthree _ = MaxThree``````
• Note: We restrict smart constructor to `InBounds`

# Example 9

Some useful auxiliary functions

``````incr :: Card n => n -> S n
incr = undefined

d0 = undefined :: Z
d1 = incr d0
d2 = incr d1
d3 = incr d2
d4 = incr d3``````

# Example 9

Testing

``````> maxthree d4

<interactive>
No instance for (InBounds Z) ..
> maxthree d1
MaxThree``````

# Example 9: conclusion

• We can perform compile-time checks on numbers

• However, it's very tedious to do that

• We can use dependently typed languages (e.g. Idris) as an alternative

# Extra example: non-empty lists

`head` and `tail` are unsafe

``````> let xs = []
> tail xs
*** Exception: Prelude.tail: empty list``````

# Extra example

We can make them safe by encoding non-emptiness in the program logic

``data NonEmpty a = a :| [a] -- Data.List.NonEmpty``
``````> let xs = 1 :| [2,3,4]
> -- provably non-empty
1``````
• Note: This can make coding more difficult!

# Extra example

Generalization using type-level numbers: `mono-traversable`

``````cadr :: MinLen (Succ (Succ nat)) [a] -> a
``````> let xs = mlcons 3 \$ mlcons 2 \$ toMinLenZero []
2``````

# Extra example

Generalization using type-level numbers: `mono-traversable`

``````-- this fails at compile-time!
> let xs = mlcons 2 \$ toMinLenZero []