[Haskell] On computable types. II. Flipping the arrow

[oleg at pobox.com]

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.


> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module TypeFN where

> import TypeLC                 -- Load part I of this series (prev message)


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:

> data Prop'
> instance A (F Prop') f (F (Prop',f))
> instance A (F (Prop',f)) Zero Bool
> instance 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
> and2 = (\x y -> x && y) `asTypeOf` (undefined:: Prop2)


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.

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

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

> oddand5 = (\x1 x2 x3 x4 -> ((x1 && x2 && x3) &&) . and2 x4)
>    `asTypeOf` oddand4t

*DepType> :t oddand4t
oddand4t :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool

We can do better, with the help of higher-order type functions.  First
we declare a few standard Haskell type constants as constants in our
calculus, with trivial evaluation rules

> instance E Bool Bool 
> instance E Int Int
> instance E String String
> instance E (a->b) (a->b)              -- We could just as well evaluate under
> instance E (a,b) (a,b)                -- these

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

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

> data ATC1 c
> instance A (F (ATC1 c)) x (c x)

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.

> type PropN' n = E(F Ntimes :< (F (ATC1 ((->) Bool))) :< Bool :< n) r => r
> and2' = (\x y -> x && y) `asTypeOf` (undefined:: PropN' N2)


To generalize,

> data ATC2 (c :: * -> * -> *)
> instance A (F (ATC2 c)) x (F (ATC1 (c x))) -- currying of type constructors

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

*TypeFN> :t test_spn4
test_spn4 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool

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

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

we make a very little change

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

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.


> data Node v els = Node v [els] deriving (Read, Show)
> type TreeDN v l n = E(F Ntimes :< (F (ATC1 (Node v))) :< l :< n) r => r
> instance E (Node v els) (Node v els)

> read_tree3 s = (read s) `asTypeOf` (undefined:: TreeDN Int String N3)

*TypeFN> :t read_tree3
read_tree3 :: String -> Node Int (Node Int (Node Int String))

> ttree3_1 = read_tree3 "Node 1 [Node 2 []]"
> ttree3_2 = read_tree3 "Node 1 [Node 2 [Node 3 [\"ok\"]]]"
> ttree3_3 = read_tree3 "Node 0 [Node 1 [Node 2 [Node 3 [\"ok\"]]]]"

*TypeFN> ttree3_2
Node 1 [Node 2 [Node 3 ["ok"]]]
*TypeFN> ttree3_3
*** Exception: Prelude.read: no parse

The ability of computed types to drive the selection of overloaded
functions has wider implications. We can remove the need for
functional dependencies, or simulate functional dependencies when they
cannot apply. For example, one may define a multi-parameter typeclass
but cannot assert functional dependencies, because not all instances
satisfy them.  Therefore, using the methods of the class may require
complex and annoying type annotations. Computed types remove the need
to manually write these annotations; the typechecker can compute them
itself.  This subject is to be explored further.

The last example showed computations of polymorphic types, which,
unsurprisingly, have the form of type abstractions. Our calculus is
built around the deep connection between type
abstraction/instantiation and functional abstraction/application.