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.