[Haskell] Re: Functional dependencies and type inference (2)

[oleg at pobox.com]

Louis-Julien Guillemette wrote:
> Say we are using a GADT to represent a simple language of boolean
> constants and conditionals,
>
> data Term a where
>    B    :: Bool -> Term Bool
>    Cnd  :: Term Bool -> Term t -> Term t -> Term t
>
> and we would like to perform a type-safe CPS conversion over this
> language. We encode the relationship between the types in the source
> language and those in the CPS-converted language using a class and a
> fundep:

Here's the code that seems to do what you wished. Liberty is taken
to extend the language so we can CPS convert more interesting terms.

Here are the tests

> term1 = Cnd (Cnd (B True) (B False) (B False)) (B True) (B False)
> test1 = shw (cps term1 id) ""

*CPS> test1
"Cnd (B True)(Cnd (B False)(B True)(B False))(Cnd (B False)(B True)(B False))"

> term2 = Cnd (Cmp (Cnd (B True) (I 1) (I 2)) (I 3)) 
> 	(B True) (Cmp (B True) (B False))
> test2 = shw (cps term2 id) ""

*CPS> test2
"Cnd (B True)(Cnd (Cmp (I 1)(I 3))(B True)(Cmp (B True)(B False)))
             (Cnd (Cmp (I 2)(I 3))(B True)(Cmp (B True)(B False)))"

The code:

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module CPS where

data Term a where
   B    :: Bool -> Term Bool
   Cnd  :: Term Bool -> Term t -> Term t -> Term t
   I    :: Int -> Term Int
   Cmp  :: Term t -> Term t -> Term Bool

-- Note the polymorphic answertype
class CpsForm t cps_t | t -> cps_t where
    cps :: Term t -> (Term cps_t -> Term w) -> Term w

instance CpsForm t t where
    cps (B b) c = c (B b)
    cps (I b) c = c (I b)
    cps (Cnd p q r) c = cps p (\p' -> Cnd p' (cps q c) (cps r c))
    cps (Cmp p q) c = cps p (\p' -> cps q (\q' -> c (Cmp p' q')))

shw:: Term t -> String -> String
shw (B t) = ("B "++) . shows t
shw (I t) = ("I "++) . shows t
shw (Cnd p q r) = ("Cnd "++) 
		  . (showParen True (shw p))
		  . (showParen True (shw q)) 
		  . (showParen True (shw r)) 
shw (Cmp p q) = ("Cmp "++) 
		. (showParen True (shw p))
		. (showParen True (shw q)) 

term1 = Cnd (Cnd (B True) (B False) (B False)) (B True) (B False)
test1 = shw (cps term1 id) ""

term2 = Cnd (Cmp (Cnd (B True) (I 1) (I 2)) (I 3)) 
	(B True) (Cmp (B True) (B False))
test2 = shw (cps term2 id) ""