-- 
-- |
-- 
-- <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.
-- 

{-# LANGUAGE KindSignatures, TypeOperators, EmptyDataDecls, Rank2Types #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances  #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.TypeFN where

import Language.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))


-- | 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.
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