{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- Type-level Typeable
-- A small type-level functional programming library

module TTypeable where

{-
 It helps in understanding the code if we imagine Haskell had 
 algebraic data kinds. We could then say

kind TyCon_name -- name associated with each (registered) type constructor

kind NAT        -- Type-level natural numbers
kind BOOL       -- Type-level booleans

kind LIST a = NIL | a :/ LIST a

-- Type-level type representation
kind TYPEREP = (TyCon_name, LIST TYPEREP)
-}

-- Type-lever typeOf
-- The more precise kind is * -> TYPEREP
type family TYPEOF ty :: *


-- Auxiliary families

-- The more precise kind is TyCon_name -> NAT
type family TC_code tycon :: *


-- Sample type reps (the rest should be derived, using TH, for example)
-- Alternatively, it would be great if GHC could provide such instances
-- automatically or by demand, e.g.,
-- deriving instance TYPEOF Foo

data ANY 				-- The wildcard, for matching
data ANY2 a

data TRN_any
type instance TC_code TRN_any = Z       -- distinguished for TRN_any
type instance TYPEOF ANY = (TRN_any, NIL)
type instance TYPEOF (ANY2 a) = (TRN_any, NIL)

data TRN_unit
type instance TC_code TRN_unit = S (TC_code TRN_any)
type instance TYPEOF () = (TRN_unit, NIL)

data TRN_bool
type instance TC_code TRN_bool = S (TC_code TRN_unit)
type instance TYPEOF Bool = (TRN_bool, NIL)

data TRN_char
type instance TC_code TRN_char = S (TC_code TRN_unit)
type instance TYPEOF Char = (TRN_char, NIL)

data TRN_int
type instance TC_code TRN_int = S (TC_code TRN_char)
type instance TYPEOF Int = (TRN_int, NIL)

data TRN_list
type instance TC_code TRN_list = S (TC_code TRN_int)
type instance TYPEOF [a] = (TRN_list, (TYPEOF a) :/ NIL)

data TRN_maybe
type instance TC_code TRN_maybe = S (TC_code TRN_list)
type instance TYPEOF (Maybe a) = (TRN_maybe, (TYPEOF a) :/ NIL)

data TRN_IO
type instance TC_code TRN_IO = S (TC_code TRN_maybe)
type instance TYPEOF (IO a) = (TRN_IO, (TYPEOF a) :/ NIL)

data TRN_arrow
type instance TC_code TRN_arrow = S (TC_code TRN_IO)
type instance TYPEOF (a -> b) = (TRN_arrow, (TYPEOF a) :/ (TYPEOF b) :/ NIL)


-- Type-level booleans

data HTrue
data HFalse

instance Show HTrue  where show _ = "HTrue"
instance Show HFalse where show _ = "HFalse"

-- BOOL -> BOOL -> BOOL
type family AND x y :: *

type instance AND HFalse x     = HFalse
type instance AND HTrue HFalse = HFalse
type instance AND HTrue HTrue  = HTrue


-- Type-level natural numbers

data Z
data S a


-- More-precise kind: NAT -> NAT -> BOOL
type family NatEq x y :: *

type instance NatEq Z Z         = HTrue
type instance NatEq Z (S x)     = HFalse
type instance NatEq (S x) Z     = HFalse
type instance NatEq (S x) (S y) = NatEq x y


-- Type-level lists

data NIL
data h :/ t
infixr 5 :/

-- LIST a -> NAT
type family Length x :: *

type instance Length NIL      = Z
type instance Length (h :/ t) = S (Length t)



-- Comparison predicate on TYPEREP and its parts


-- TYPEREP -> TYPEREP -> BOOL
type family TREPEQ x y :: *

type instance TREPEQ (tc1, targ1) (tc2, targ2) =
    AND (NatEq (TC_code tc1) (TC_code tc2))
	(TREPEQL targ1 targ2)

-- LIST TYPEREP -> LIST TYPEREP -> BOOL
type family TREPEQL xs ys :: *

type instance TREPEQL NIL NIL      = HTrue
type instance TREPEQL NIL (h :/ t) = HFalse
type instance TREPEQL (h :/ t) NIL = HFalse
type instance TREPEQL (h1 :/ t1) (h2 :/ t2) = 
    AND (TREPEQ h1 h2) (TREPEQL t1 t2)

-- Matching: comparison that takes wildcards into account
-- The code is written less elegantly for speed

type family TREPEQW x y :: *

type instance TREPEQW (tc1, targ1) (tc2, targ2) =
  TREPEQW' (TC_code tc1) (TC_code tc2) targ1 targ2

-- NAT -> NAT -> LIST TYPEREP -> LIST TYPEREP -> BOOL
type family TREPEQW' c1 c2 arg1 arg2 :: *

-- Wildcard, with the code 0, always matches
type instance TREPEQW' Z c2     arg1 arg2 = HTrue
type instance TREPEQW' (S c1) Z arg1 arg2 = HTrue
type instance TREPEQW' (S c1) (S c2) arg1 arg2 =
    AND (NatEq c1 c2) (TREPEQLW arg1 arg2)

-- LIST TYPEREP -> LIST TYPEREP -> BOOL
type family TREPEQLW xs ys :: *

type instance TREPEQLW NIL NIL      = HTrue
type instance TREPEQLW NIL (h :/ t) = HFalse
type instance TREPEQLW (h :/ t) NIL = HFalse
type instance TREPEQLW (h1 :/ t1) (h2 :/ t2) = 
    AND (TREPEQW h1 h2) (TREPEQLW t1 t2)

-- Higher-order type-level functions

type family Apply lab arg :: *

data AC_TREPEQ
type instance Apply AC_TREPEQ (x,y) = TREPEQ x y
data AC_TREPEQW
type instance Apply AC_TREPEQW (x,y) = TREPEQW x y

data CLOS x arg
type instance Apply (CLOS x arg) () = Apply x arg


-- Type-level membership predicate, using the given equality
-- comparison function

-- ((*,*) -> BOOL) -> * -> LIST * -> BOOL
type family Member f x l :: *

type instance Member f x NIL = HFalse
type instance Member f x (h :/ t) = 
  ORELSE (Apply f (x,h)) (CLOS AC_Member (f,x,t))

data AC_Member
type instance Apply AC_Member (x,y,z) = Member x y z

-- OR with the shortcut evaluation
type family ORELSE x y :: *

type instance ORELSE HTrue x  = HTrue
type instance ORELSE HFalse x = Apply x ()

-- example

ex1 = undefined :: TYPEOF (IO [Bool])

-- *TTypeable> :t ex1
-- ex1 :: (TRN_IO, (TRN_list, (TRN_bool, NIL) :/ NIL) :/ NIL)

ex2 = undefined :: TREPEQ (TYPEOF (IO [Bool])) (TYPEOF (IO [Bool]))
-- HTrue

ex3 = undefined :: TREPEQ (TYPEOF (IO [Bool])) (TYPEOF (IO Bool))
-- HFalse

ex4 = undefined :: TREPEQW (TYPEOF (IO [Bool])) (TYPEOF (IO ANY))
-- HTrue

ex41 = undefined :: TREPEQW (TYPEOF (IO [ANY])) (TYPEOF (IO Bool))
-- HFalse

ex42 = undefined :: TREPEQW (TYPEOF (IO [ANY])) (TYPEOF (IO [Int]))
-- HTrue

ex5 = undefined :: Member AC_TREPEQ (TYPEOF Bool)
                          (TYPEOF () :/ (TYPEOF Bool) :/ TYPEOF (IO ()) :/ NIL)
-- HTrue

ex6 = undefined :: Member AC_TREPEQ (TYPEOF (IO Bool))
                          ((TYPEOF Bool) :/ TYPEOF (IO ()) :/ NIL)

-- HFalse

ex7 = undefined :: Member AC_TREPEQW (TYPEOF (IO ANY))
                           ((TYPEOF Bool) :/ TYPEOF (IO ()) :/ NIL)

-- HTrue