Language.TypeFN

http://okmij.org/ftp/Haskell/types.html#computable-types

Part I of the series introduced the type-level functional language with the notation that resembles lambda-calculus with case distinction, fixpoint recursion, etc. Modulo a bit of syntactic tart, the language of the type functions even looks almost like the pure Haskell. In this message, we show the applications of computable types, to ascribe signatures to terms and to drive the selection of overloaded functions. We can compute the type of a tree of the depth fib(N) or a complex XML type, and instantiate the read function to read the trees of only that shape.

A telling example of the power of the approach is the ability to use not only (a->) but also (->a) as an unary type function. The former is just (->) a. The latter is considered impossible. In our approach, (->a) is written almost literally as (flip (->) a)

This series of messages has been inspired by Luca Cardelli's 1988 manuscript ``Phase Distinctions in Type Theory'' http://lucacardelli.name/Papers/PhaseDistinctions.pdf and by Simon Peyton Jones and Erik Meijer's ``Henk: A Typed Intermediate Language'' http://www.research.microsoft.com/~simonpj/Papers/henk.ps.gz which expounds many of the same notions in an excellent tutorial style and in modern terminology.

I'm very grateful to Chung-chieh Shan for pointing out these papers to me and for thought-provoking discussions.

Documentation

data Prop'

Our first example comes from Cardelli's paper: defining the type Prop(n), of n-ary propositions. That is,

   Prop(2) should be the type       Bool -> Bool -> Bool
   Prop(3) is the type of functions Bool -> Bool -> Bool -> Bool

etc.

Cardelli's paper (p. 10) writes this type as

let Prop:: AllKK(N:: NatK) Type =
     recK(F:: AllKK(N:: NatK) Type)
         funKK(N:: NatK) caseK N of 0K => Bool; succK(M) => Bool -> F(M);

let and2: Prop(2K) =
     fun(a: Bool) fun(b: Bool) a & b;

Here 0K and 2K are type-level numerals of the kind NatK; recK is the type-level fix-point combinator. The computed type Prop(2) then gives the type to the term and2.

In our system, this example looks as follows:

Instances

A (F (Prop', f)) Zero Bool

A (F Prop') f (F (Prop', f))

E (:< f m) r => A (F (Prop', f)) (Su m) (Bool -> r)

type Prop = Rec (F Prop')

type Prop2 = E (F Prop :< N2) r => r

data StrangeProp

We can compute types by applying type functions, just as we can compute values by applying regular functions. Indeed, let us define a StrangeProp of the kind NAT -> Type. StrangeProp(n) is the type of propositions of arity m, where m is fib(n). We compose together the already defined type function Prop2 and the type function Fib in the previous message.

Instances

E (:< (F Prop) (:< (F Fib) n)) r => A (F StrangeProp) n r

oddand4t :: E (F StrangeProp :< ((F FSum :< N2) :< N2)) r => r

data Ntimes

We introduce the combinator Ntimes: |NTimes f x n| applies f to x n times. This is a sort of fold over numerals.

Instances

A (F (Ntimes, f, x)) Zero x

A (F (Ntimes, f)) x (F (Ntimes, f, x))

A (F Ntimes) f (F (Ntimes, f))

E (:< (:< (:< (F Ntimes) f) (:< f x)) n) r => A (F (Ntimes, f, x)) (Su n) r

data ATC1 c

Instances

A (F (ATC2 c)) x (F (ATC1 (c x)))

A (F (ATC1 c)) x (c x)

type PropN' n = E (((F Ntimes :< F (ATC1 ((->) Bool))) :< Bool) :< n) r => r

We can then write the type of n-ary propositions Prop(N) in a different way, as an N-times application of the type constructor (Bool->) to Bool.

data ATC2 c

To generalize,

Instances

A (F (ATC2 c)) x (F (ATC1 (c x)))

type SPropN' n = E (((F Ntimes :< (F (ATC2 (->)) :< Bool)) :< Bool) :< (F Fib :< n)) r => r

data Flip

The comparison of ATC1 with ATC2 shows two different ways of defining abstractions: as (F x) terms (`lambda-terms' in our calculus) and as polymorphic types (Haskell type abstractions). The two ways are profoundly related. The more verbose type application notation, via (:<), has its benefits. After we introduce another higher-order function

Instances

E (:< (:< f y) x) r => A (F (Flip, f, x)) y r

A (F (Flip, f)) x (F (Flip, f, x))

A (F Flip) f (F (Flip, f))

type SSPropN' n = E (((F Ntimes :< ((F Flip :< F (ATC2 (->))) :< Bool)) :< Bool) :< (F Fib :< n)) r => r

we make a very little change

data Node v els

and obtain quite a different result:

 *TypeFN> :t test_sspn4
 test_sspn4 :: ((((Bool -> Bool) -> Bool) -> Bool) -> Bool) -> Bool

In effect, we were able to use not only (a->) but also (->a) as an unary type function. Moreover, we achieved the latter by almost literally applying the flip function to the arrow type constructor (->).

Using the type inspection tools (typecast), we can replace the family of functions ATC1, ATC2 with one, kind-polymorphic, polyvariadic function ATC. This approach will be explained in further messages.

We can use the computed types to drive overloaded functions such as read and show. The specifically instantiated read functions, in particular, will check that a (remotely) received serialized value matches our expectation. Let's consider the type of trees of the depth of at most N.

Constructors

Node v [els]

Instances

(Read v, Read els) => Read (Node v els)

(Show v, Show els) => Show (Node v els)

E (Node v els) (Node v els)

type TreeDN v l n = E (((F Ntimes :< F (ATC1 (Node v))) :< l) :< n) r => r