Created
September 19, 2010 09:10
-
-
Save spockz/586611 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data UnitT = Unit deriving Show | |
data Sum aT bT = Inl aT | Inr bT deriving Show | |
data Prod aT bT = Prod aT bT deriving Show | |
data EP bT cT = EP {from :: (bT -> cT), to :: (cT -> bT)} | |
data Rep tT where | |
RUnit :: Rep UnitT | |
RInt :: Rep Int | |
RChar :: Rep Char | |
RSum :: Rep aT -> Rep bT -> Rep (Sum aT bT) | |
RProd :: Rep aT -> Rep bT -> Rep (Prod aT bT) | |
RString :: Rep String | |
RCon :: String -> Rep aT -> Rep aT | |
RType :: EP bT cT -> Rep cT -> Rep bT | |
type RepAlgebra r = (r | |
,r | |
,r | |
,r | |
,forall a b. a -> b -> r | |
,forall a b. a -> b -> r | |
,forall a . String -> a -> r | |
,forall a b. EP a b -> r -> r | |
) | |
-- This works, but is extremely bloated, ugly, and plain yuk | |
foldRep :: RepAlgebra r -> Rep a -> r | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RUnit) = unit | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RInt) = int | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RChar) = char | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RString) = string | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RSum ra rb) = sum (foldRep a ra) (foldRep a rb) | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RProd ra rb) = prod (foldRep a ra) (foldRep a rb) | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RCon l ra) = con l (foldRep a ra) | |
foldRep a@(unit, int, char, string, sum, prod, con, t) (RType ep ra) = t ep (foldRep a ra) | |
-- This doesn't compile: | |
foldRep' :: RepAlgebra r -> Rep a -> r | |
foldRep' (unit, int, char, string, sum, prod, con, t) = f | |
where | |
f (RUnit) = unit | |
f (RInt) = int | |
f (RChar) = char | |
f (RString) = string | |
f (RSum ra rb) = sum (f ra) (f rb) | |
f (RProd ra rb) = prod (f ra) (f rb) | |
f (RCon l ra) = con l (f ra) | |
f (RType ep ra) = t ep (f ra) | |
{- | |
GADT pattern match in non-rigid context for `RUnit' | |
Probable solution: add a type signature for `f' | |
In the pattern: RUnit | |
In the definition of `f': f (RUnit) = unit | |
In the definition of `foldRep': | |
foldRep (unit, int, char, string, sum, prod, con, t) | |
= f | |
where | |
f (RUnit) = unit | |
f (RInt) = int | |
f (RChar) = char | |
f (RString) = string | |
f (RSum ra rb) = sum (f ra) (f rb) | |
f (RProd ra rb) = prod (f ra) (f rb) | |
f (RCon l ra) = con l (f ra) | |
f (RType ep ra) = t ep (f ra) | |
-} | |
-- Adding the type doesn't help, how can I convince the compiler that r in the type of f is the same as in the type of foldRep'? | |
foldRep' :: RepAlgebra r -> Rep a -> r | |
foldRep' (unit, int, char, string, sum, prod, con, t) = f | |
where f :: Rep a -> r | |
f (RUnit) = unit | |
f (RInt) = int | |
f (RChar) = char | |
f (RString) = string | |
f (RSum ra rb) = sum (f ra) (f rb) | |
f (RProd ra rb) = prod (f ra) (f rb) | |
f (RCon l ra) = con l (f ra) | |
f (RType ep ra) = t ep (f ra) | |
{- | |
Couldn't match expected type `r1' against inferred type `r' | |
`r1' is a rigid type variable bound by | |
the type signature for `f' at gadtalgebra.hs:67:22 | |
`r' is a rigid type variable bound by | |
the type signature for `foldRep'' at gadtalgebra.hs:65:23 | |
In the expression: t ep (f ra) | |
In the definition of `f': f (RType ep ra) = t ep (f ra) | |
In the definition of `foldRep'': | |
foldRep' (unit, int, char, string, sum, prod, con, t) | |
= f | |
where | |
f :: Rep a -> r | |
f (RUnit) = unit | |
f (RInt) = int | |
f (RChar) = char | |
f (RString) = string | |
f (RSum ra rb) = sum (f ra) (f rb) | |
f (RProd ra rb) = prod (f ra) (f rb) | |
f (RCon l ra) = con l (f ra) | |
f (RType ep ra) = t ep (f ra) | |
-} | |
-- And now with the ScopedTypeVariables extension: | |
foldRep' :: forall r a. RepAlgebra r -> Rep a -> r | |
foldRep' (unit, int, char, string, sum, prod, con, t) = f | |
where f :: Rep a -> r | |
f (RUnit) = unit | |
f (RInt) = int | |
f (RChar) = char | |
f (RString) = string | |
f (RSum ra rb) = sum (f ra) (f rb) | |
f (RProd ra rb) = prod (f ra) (f rb) | |
f (RCon l ra) = con l (f ra) | |
f (RType ep ra) = t ep (f ra) | |
{- | |
Occurs check: cannot construct the infinite type: aT = Sum aT bT | |
In the pattern: RSum ra rb | |
In the definition of `f': f (RSum ra rb) = sum (f ra) (f rb) | |
In the definition of `foldRep'': | |
foldRep' (unit, int, char, string, sum, prod, con, t) | |
= f | |
where | |
f :: Rep a -> r | |
f (RUnit) = unit | |
f (RInt) = int | |
f (RChar) = char | |
f (RString) = string | |
f (RSum ra rb) = sum (f ra) (f rb) | |
f (RProd ra rb) = prod (f ra) (f rb) | |
f (RCon l ra) = con l (f ra) | |
f (RType ep ra) = t ep (f ra) | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment