1
|
- Tim Sheard
- Portland State University
- (formerly from OGI/OHSU)
|
2
|
- Inductively formed structured data
- Generalizes enumerations & tagged variants
- Types used to prevent the construction of ill-formed data
- Pattern matching allows abstract high level (yet still efficient) access
- Can be parameterized to make polymorphic container-like structures
|
3
|
- Data Tree a
- = Fork (Tree a) (Tree a)
- | Node a
- | Tip
- Fork :: Tree a -> Tree a -> Tree a
- Node :: a -> Tree a
- Tip :: Tree a
|
4
|
- We would like the parameter of a type constructor (e.g. the “a” in “T
a”) to say something about the values with type “T a”
- phantom types
- indexed types
- Imagine a type-indexed Term datatype
- Int :: Int -> Term Int
- Bool :: Bool -> Term Bool
- Plus :: Term Int -> Term Int -> Term Int
- Less :: Term Int -> Term Int -> Term Bool
- If :: Term Bool -> Term a -> Term a -> Term a
|
5
|
- Benefits
- The type system disallows ill-formed Terms like:
- (If (Int 3) (Int 0) (Int 9))
- Documentation
- Problems
- How do we type pattern matching?
- case x of
- (Int n) -> . . .
- (Bool b)-> . . .
- What type is x?
|
6
|
- Data Term a
- = Int Int where a=Int
- | Bool Bool where a=Bool
- | Plus (Term Int) (Term Int) where
a=Int
- | Less (Term Int) (Term Int) where
a=Bool
- | If (Term Bool) (Term a) (Term
a)
- Int :: forall a.(a=Int) => Int -> Term a
- We can specialize this kind of type to the ones we want
- Int :: Int -> Term Int
- Bool :: Bool -> Term Bool
- Plus :: Term Int -> Term Int -> Term Int
- Less :: Term Int -> Term Int -> Term Bool
- If :: Term Bool -> Term a -> Term a -> Term a
|
7
|
- eval :: Term a -> a
- eval (Int n) = n
- eval (Bool b) = b
- eval (Plus x y) = eval x + eval y
- eval (Less x y) = eval x < eval y
- eval (If x y z) =
- if (eval x)
- then (eval y)
- else (eval z)
|
8
|
- eval :: Term a -> a
- eval (Less x y) = eval x < eval y
- Less::(a=Bool)=>Term Int -> Term Int -> Term Bool
- x :: Term Int
- y :: Term Int
- (eval x) :: Int
- (eval y) :: Int
- (eval x < eval y) :: Bool
|
9
|
- Allow algebraic definitions to define new “kinds” as well as new “types”
- The primitive kind: *
- 5 :: Int :: *
- [Int] :: *
- [] :: * ~> *
- Kind Nat = Zero | Succ Nat
- Zero :: Nat
- Succ :: Nat ~> Nat
- Succ Zero :: Nat
|
10
|
|
11
|
- Data is a parameterized generalized-algebraic datatype
- It is indexed by some semantic property
- New Kinds introduce new types that are used as indexes
- Programs use types to maintain semantic properties
- The equality constrained types make it possible
|
12
|
- Typed Lambda Calculus
- A Language with Security Domains
- A Language which enforces an interaction protocol
|
13
|
- data V s t
- = ex m . Z where s = (t,m)
- | ex m x . S (V m t) where s =
(x,m)
- data Exp s t
- = IntC Int where t = Int
- | BoolC Bool where t = Bool
- | Plus (Exp s Int) (Exp s Int) where
t = Int
- | Lteq (Exp s Int) (Exp s Int) where
t = Bool
- | Var (V s t)
- Example Type:
- Plus :: forall s t . (t=Int) =>
- Exp s Int ->
Exp s Int -> Exp s t
|
14
|
- kind Domain = High | Low
- data D t
- = Lo where t = Low
- | Hi where t = High
- data Dless x y
- = LH where x = Low , y = High
- | LL where x = Low, y = Low
- | HH where x = High, y = High
- data Exp s d t
- = Int Int where t = Int
- | Bool Bool where t = Bool
- | Plus (Exp s d Int) (Exp s d
Int) where t = Int
- | Lteq (Exp s d Int) (Exp s d
Int) where t = Bool
- | forall d2 . Var (V s d2 t)
(Dless d2 d)
|
15
|
- kind State = Open | Closed
- data V s t
- = forall st . Z where s = (t,st)
- | forall st t1 . S (V st t)
- where s =
(t1,st)
- data Com st x y
- = forall t . Set (V st t) (Exp
st t) where x=y
- | forall a . Seq (Com st x a)
(Com st a y)
- | If (Exp st Bool) (Com st x y)
(Com st x y)
- | While (Exp st Bool) (Com st x
y) where x = y
- | forall t . Declare (Exp st t)
(Com (t,st) x y)
- | Open where x = Closed, y =
Open
- | Close where x = Open, y =
Closed
- | Write (Exp st Int) where x = Open, y = Open
|
16
|
- Build heterogeneous meta-programming systems
- Meta-language ≠ object-language
- Type system of the meta-language guarantees semantic properties of
object-language
- Experiment with Omega
- Finding new uses for the power of the type system
- Translating existing language-based ideas into Omega
- staged interpreters
- proof carrying code
- language-based security
|
17
|
- Wmega’s type system is good
for statically guaranteeing all sorts of properties.
- Lists with statically known length
- Red–Black Trees
- Binomial Heaps
- Dynamic Typing
|
18
|
- A kind of natural numbers
- Classifies types Z, S Z, S (S Z)…
- These types do not classify any runtime computations
- Lists with length n
- List a n: list with objects of
type “a” whose length is “n”
- Equality qualifications constrain types
- A list (Cons x xs) has the type (List a (S m)) provided that the list xs
has the type (List a m)
|
19
|
- Cons :: (n=(S m)) =>a -> (Seq a m) -> (Seq a n)
- When applying a constructor, the equality must be satisfied from a set
of known facts
- Given x : a,
- y : Seq a m
- Cons x y :: Seq a n
- Provided we can prove the obligation:
n=S m
- New known facts are introduced when pattern matching against a qualified
constructor
- The defintion: f ((Cons x
y)::Seq a n) = . . .
- x::a, y::Seq a m and the fact that n=S m
- Equalities in obligations are solved using the facts by a decision
procedure
|
20
|
- The function map preserves the
length of lists
|
21
|
- (List a m) -> (List a n) -> (List a (m+n))
- What is (m + n) ?
- It’s not an application of a type constructor
- It’s an application of a type-function
- How is it defined
- How is append type checked?
|
22
|
- sum :: Nat ~> Nat ~> Nat
- {sum Z x} = x
- {sum (S x) y} = S {sum x y}
- append :: List a n ->
- List a m ->
- List a {sum n m}
- append Nil ys = ys
- append (Cons x xs) ys = Cons x (append xs ys)
|
23
|
- Stating static properties is a good way to think about programming
- It may lead to more reliable programs
- The compiler should ensure that programs maintain the stated properties
- Generalizing algebraic datatypes make it all possible
- Ranges other than “T a”
- “a” becomes an index describing a static property of x::T a
- New kinds let “a” have arbitrary structure
- Computing over “a” is sometimes necessary
|
24
|
- Typed, staged interpreters
- For languages with binding, with patterns, algebraic datatypes
- Type preserving transformations
- Simplify :: Exp t -> Exp t
- Cps:: Exp t -> Exp {trans t}
- Proof carrying code
- Data Structures
- Red-Black trees, Binomial Heaps , Static length lists
- Languages with security properties
- Typed self-describing databases, where meta data in the database
describes the database schema
- Programs that slip easily between dynamic and statically typed sections.
Type-case is easy to encode with no additional mechanism
|