{-# 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