On the theory side:

• intersection types
• union types
• bounded quantification
• soft-typing like type inference
• no conditional constraints
• no flow analysis (but uses fresh types per each pattern in pattern matching matches)

Very brief syntax explaination

operators

Types of simple expressions

first order

simple functions

functions using pattern matching

Naming types

Bool = True | False
Maybe(x) = None | Some(x)

• [ Leaf(1), Leaf(True) ] is a valid expression
• but it isn't valid anymore if a type Tree = Leaf(0|1) | Node(Tree, Tree) has been declared.
• it is valid again if another type TreeB = Leaf(True) | Node(TreeB, TreeB) has been declared.

Some other common types:

Byte = Builtin::Or_range(0, 255)
Uint = Builtin::Or_range(0, 2147483647) # 2**31 - 1
Int = Builtin::Or_range(-2147483648, 2147483647)
Char = Builtin::Or_range("\x00", "\xff") # 8bit chars, to be extended with Unicode
# Float *could* be described as follow:
# Float = (list_product(-2**52 .. 2**52-1, -2**10+1 .. 2**10-1)).map(mant,exp -> mant / 2**51 * 2**exp).range

• Char < String (where String is the infinite union of strings)
• Byte < Uint < Int
• Int < Integer < Rational (where Integer is math Z, Rational is math Q)
• Int < Float < Rational (note that Float really are C's double, and do include 32 bits integers)

Type constraints

function call

assignment

bounded polymorphism

Intersection values

not := True -> False ;; False -> True
#                                       which implies  not !! Bool -> Bool
inv := 0 -> 1 ;; 1 -> 0
#                                       which implies  inv !! 0|1 -> 0|1
i !< 0|1
b !< Bool

overloading ad'hoc

records

free intersection values

• 1|&|"foo" + 1|&|"bar" gives 2|&|"foobar"
• [ 1, "foo" ].map(x -> x + 1|&|"bar") gives [ 2, "foobar" ]
• 0 |&| "" |&| [] as a default value to initialize variables
• (min, sec) = s.m("(\d+):(\d+)") is a regexp returning type Int|&|String, Int|&|String.
  This enables:
  • min * 60 + sec where min and sec are used as numbers
  • print_string(min)

abstract types

Abstract types

• being types, they can only be manipulated at compile-time (they still are first class values)
• they are not manipulated directly, but using a little sugar
• together with Open_function, they can achieve mix-ins (aka type classes)
• implementation subtyping is used (thick arrows on the diagram)

Simple example

Addable = class
    ::+ := o,o -> o
    # removed += times  to simplify

Addable = &Addable
::+ := Open_function(o,o -> (o !< Addable) ; o)

• x -> x + 1 !! x -> (x !> 1) ; (x !< Addable) ; x
  # when going closed world:
             !! x -> (x !> 1) ; (x !< Rational) ; x
    

  Rational is chosen here as the upper-bound of the various types verifying lower bounded by 1 and upper bounded by Addable. Strings and lists are discarded.

•   
  x -> x + 1|&|"foo" !! x -> (x !> 1|&|"foo") ; (x !< Addable) ; x
  # when going closed world:
                     !! x -> (x !> 1|&|"foo") ; (x !< Rational | String) ; x
    

Interface inheritance

Eq = class
    ::== := o,o -> Bool
    ::!= := o,o -> Bool

Ordered = Eq |&| class
    ::<=> := o,o -> -1|0|1
    ::<   := o,o -> Bool
    # removed <= > >= min max  to simplify

Eq = &Eq
::== := Open_function(o,o -> (o !< Eq) ; Bool)
::!= := Open_function(o,o -> (o !< Eq) ; Bool)

Ordered = Eq |&| &Ordered
::<=> := Open_function(o,o -> (o !< Ordered) ; -1|0|1)
::<   := Open_function(o,o -> (o !< Ordered) ; Bool)

a == b := a<=>b == 0

Covariance, invariance

Covariance and Contravariance, Distributivity?

Problem

Answer

• [ 1, "foo" ] is not a List(Int) | List(String)
• [ 1, "foo" ] is a List(Int | String)

Question

Examples

• Maybe

  Maybe(a) = None | Some(a)
  aka Maybe = (_ -> None) | Some
  
  Maybe(a) | Maybe(b)
  = (None | Some(a)) | (None | Some(b))
  =  None | Some(a)  |  None | Some(b)
  =  None | Some(a) | Some(b)
  =  None | Some(a|b)
  =  Maybe(a|b)
  

• AB

  AB(a) = A(a) | B(a)
  aka AB = A | B
  
  AB(a) | AB(b)
  = (A(a) | B(a)) | (A(b) | B(b))
  =  A(a) | A(b)  |  B(a) | B(b)
  =    A(a|b)     |    B(a|b)
  =           AB(a|b)
  

• AA

  AA(a) = A(a,a)
  
  AA(a) | AA(b)
  =  A(a,a) | A(b,b)
  =  A( (a,a) | (b,b) )
  <> A(a|b, a|b)
  since (a,a) | (b,b)  !<  (a|b,a|b)
    but (a,a) | (b,b)  !>  (a|b,a|b)  is false
  
  eg: (1|2, 1|2)  is  (1, 1) | (1, 2) | (2, 1) | (2, 2)  
                  !>  (1, 1) | (2, 2)
  

• List

  List(a) = Nil | Cons(a, List(a))
  
  List(a) | List(b)
  = (Nil | Const(a, List(a))) | (Nil | Const(b, List(b)))
  =  Nil | Const(a, List(a))  |  Nil | Const(b, List(b))
  =  Nil | Const(a, List(a)) | Const(b, List(b))
  =  Nil | Const( (a, List(a)) | (b, List(b)) )
  <> Nil | Const(a|b, List(a|b)) 
  
  

Conclusion

• it works for "Maybe" ("Some" uses ony one "a", "None" uses none)
• it works for "AB" (both "A" and "B" use only one "a")
• it fails for "AA" and "List"

Terminology

Mutability

Inout

  t1 !< Inout(t2) implies t1 !! t2
  t1 !> Inout(t2) implies t1 !! t2

• beware of common place errors:
  • record subtyping (aka data inheritance)

        Inout(X(Int) /\ Y(Int))  <  Inout(X(Int))  is *false*
       but
        X(Inout(Int)) /\ Y(Inout(Int))  <  X(Inout(Int))  is true!
    

    so no need for a special ugly rule for data inheritance.
  • containers subtyping

        Inout(List(car))  <  Inout(List(vehicle))  is *false*
        List(Inout(car))  <  List(Inout(vehicle))  is *false*
       but
        List(car)  <  List(vehicle)  is true!
        List(X(Inout(Int)) /\ Y(Inout(Int)))  <  List(X(Inout(Int)))  is true!
          (since List(X(Inout(Int)) /\ Y(Inout(Int))) = List(X(Inout(Int))) /\
          List(Y(Inout(Int)))) 
    

  OO languages have a hard time with this since they usually do not make the difference between mutable and non-mutable data.

Out

References

• Introduction to types
  • Types in Programming Languages
• Union and intersection types
  • Programming With Intersection Types, Union Types, and Polymorphism
  • Types récursifs, combinaisons booléennes et fonctions surchargées
• Bounded polymorphism
  • On Understanding Types, Data Abstraction, and Polymorphism
  • Programming with Intersection Types and Bounded Polymorphism
• Intersection values
  • Type-indexed rows
• Precise types
  • soft-typing
    • Cartwright and Fagan (1991)
    • Mr. Spidey for Scheme using constraint-based flow analysis.
    • Selectors Make Analysing "case-lambda" Too Hard
    • MrFlow: Why MrSpidey Failed
    • How to combine the benefits of strict and soft typing
    • in erlang
    • cons, cons2 (somewhat old)

Release: $Id: types.html,v 1.12 2003/01/09 18:30:56 pixel_ Exp $