Type Constraints for Data Constructors

So we know how to use a type parameter to statically constrain the length of a list.  Let’s continue our exploration of type constraints and see if we can figure out how to constrain the return type of a data constructor.

 

Data Constructor Constraints in Haskell

 

The paper “Fun with Phantom Types” by R Hinze has an example of a simple expression language in Haskell.

 

data Term t = Zero

            | Succ(Term Int)

            | Pred(Term Int)

            | IsZero(Term Int)

            | If (Term Bool) (Term t) (Term t)

 

What we’d like to be able to do with this language is have the interpreter statically catch any type errors.  For instance,

 

Main>let one = Succ(Zero)

Main>eval IsZero(one)

 

is a type safe declaration because IsZero can take a Term Int, whereas

 

Main>IsZero(IsZero one)

 

is not type safe because IsZero does not take a Term Bool.  Hinze suggest the following ‘mild’ extension for Haskell.

 

data Term t = Zero                             with t = Int

            | Succ(Term Int)                   with t = Int

            | Pred(Term Int)                   with t = Int

            | IsZero(Term Int)                 with t = Bool

            | If (Term Bool) (Term a) (Term a) with t = a

 

What the extension does is constrain each type constructor to returning a Term of the type specified after the with keyword.  Let’s see how we could do this in F#

 

Data Constructor Constraints in F#

 

We’ll start by building a discriminated union to construct our Term.

 

type Term<’t> = Zero

              | Succ of Term<int>

              | Pred of Term<int>

              | IsZero of Term<bool>

              | If of Term<bool> * Term<’t> * Term<’t>

 

And let’s examine the types when we use our union.

 

// val one : Term<’a>

let one = Succ(Zero)

// val is_false : Term<’a>

let is_false = IsZero(one)

// val is_problem : Term<’a>

let is_problem = IsZero(IsZero(one))

 

Notice how each of our bound variables gets assigned the type Term<a>?  What we would prefer is for the F# compiler to constrain the return type of the constructor to a designated type. This would allow the compiler to catch the type error on line 3.  An IsZero can only accept Term<int> and here we’re passing it a Term<bool>. 

 

So if we can’t fool the compiler at link time then let’s at least force a runtime exception.

 

let rec eval (t : Term<’a>) =

    match t with

    | Zero         -> 0

    //this code causes the construct to be less generic than the annotation

    | Succ e       -> eval e + 1

    | Pred e       -> eval e – 1

    //the expression has type bool but here is used with type int

    | IsZero e     -> eval e = 0

    | If(e1,e2,e3) -> if eval e1 then eval e2 else eval e3         

 

No such luck.  The match on Succ constrains t to Term<int> which prevents us from passing e to the eval statement at the IsZero match.  The type inference algorithm does not allow for polymorphic inputs or outputs to functions.  Why not?  Remember from this blog entry that “match” functions get compiled down into standard .Net methods.  So what language does allow for polymorphic return types?

 

Data Constructor Constraints in VB

 

Let’s dust off our old standby and see if it can’t teach the Haskell and F# prodigies a lesson on problem solving.

 

Public MustInherit Class Term(Of TEval)

    Public MustOverride Function Eval() As TEval

End Class

 

Public Class Succ

    Inherits Term(Of Integer)

    Private _e As Term(Of Integer)

    Public Sub New(ByVal e As Term(Of Integer))

        _e = e

    End Sub

    Public Overrides Function Eval() As Integer

        Return _e.Eval + 1

    End Function

End Class

 

Public Class IsZero

    Inherits Term(Of Boolean)

    Private _e As Term(Of Integer)

    Public Sub New(ByVal e As Term(Of Integer))

        _e = e

    End Sub

    Public Overrides Function Eval() As Boolean

        Return _e.Eval = 0

    End Function

End Class

 

The constructor for each of our terms does allow us to constrain the type of term that can be used to construct the term.  The TEval type constraint further lets us constrain the type that gets returned when the type is evaluated.

 

All we’ve done is break our constructor and eval function out over each term.  Because each term has its own slot in the virtual method table our “broken out” function can return a different type depending upon the match.  It seems odd that F# does something very similar to the above when building discriminated unions but chooses to combine the eval function into a single function instead of making the match code local to each term.

 

//why is the code to right of the -> not encapsulated in each term?

let rec eval (t : Term<’a>) =

    match t with

    | Zero         -> 0

    | Succ e       -> eval e + 1

    | Pred e       -> eval e – 1

    | IsZero e     -> eval e = 0

    | If(e1,e2,e3) -> if eval e1 then eval e2 else eval e3         

 

Because if it was then we’d realize the benefits of static checking for our domain specific expression languages just like the terms we constructed in VB.

 

// val one : Succ

let one = Succ(Zero())

// val is_false : IsZero

let is_false = IsZero(one)

// the type IsZero is not compatible with the type int

let is_problem = IsZero(IsZero(one))

 

Thanks for figuring that out for me compiler!  Kind of nice to see our trusty, Von Neumann, hacker language for Morts teach our lambda friends a lesson in how to do type safe domain specific languages.

 

Full Source Code

 

Public MustInherit Class Term(Of TEval)

    Public MustOverride Function Eval() As TEval

End Class

 

Public Class Zero

    Inherits Term(Of Integer)

    Public Sub New()

    End Sub

    Public Overrides Function Eval() As Integer

        Return 0

    End Function

End Class

 

Public Class Succ

    Inherits Term(Of Integer)

    Private _e As Term(Of Integer)

    Public Sub New(ByVal e As Term(Of Integer))

        _e = e

    End Sub

    Public Overrides Function Eval() As Integer

        Return _e.Eval + 1

    End Function

End Class

 

Public Class Pred

    Inherits Term(Of Integer)

    Private _e As Term(Of Integer)

    Public Sub New(ByVal e As Term(Of Integer))

        _e = e

    End Sub

    Public Overrides Function Eval() As Integer

        Return _e.Eval – 1

    End Function

End Class

 

Public Class IsZero

    Inherits Term(Of Boolean)

    Private _e As Term(Of Integer)

    Public Sub New(ByVal e As Term(Of Integer))

        _e = e

    End Sub

    Public Overrides Function Eval() As Boolean

        Return _e.Eval = 0

    End Function

End Class

 

Public Class [If](Of TEval)

    Inherits Term(Of TEval)

    Private _e1 As Term(Of Boolean)

    Private _e2 As Term(Of TEval)

    Private _e3 As Term(Of TEval)

    Public Sub New(ByVal e1 As Term(Of Boolean), ByVal e2 As Term(Of TEval), ByVal e3 As Term(Of TEval))

        _e1 = e1

        _e2 = e2

        _e3 = e3

    End Sub

    Public Overrides Function Eval() As TEval

        If _e1.Eval Then

            Return _e2.Eval

        Else

            Return _e3.Eval()

        End If

    End Function

End Class 

 

#light

 

open TermVB

 

let one = Succ(Zero())

let i = one.Eval()

printfn “%A” i

 

let i1 = IsZero(one).Eval()

printfn “%A” i1

 

// the type IsZero is not compatible with type Term<int>

//let i2 = IsZero(IsZero(one))

 

let i3 = If(IsZero(one),Zero(),one).Eval()

printfn “%A” i3

 

let True = IsZero(Zero())

let False = IsZero(one)

let t1 = If(True,True,False).Eval()

printfn “%A” t1

 

System.Console.ReadLine()