Flipping *->*->* kinds, or monadic finally-tagless madness
I'm trying to write HOAS Show instances for the finally-tagless type-classes using actual State monads. The original code: http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs Two type variables are needed: one to vary over the Symantics class (but only as a phantom type) and another to vary over the Monad class. Hence, the use of 2-variable type constructors.
type VarCount = int newtype Y b a = Y {unY :: VarCount -> (b, VarCount)}
Not knowing of a type-level 'flip', I resort to newtype isomorphisms:
newtype Z a b = Z {unZ :: Y b a} instance Monad (Z a) where return x = Z $ Y $ \c -> (x,c) (Z (Y m)) >>= f = Z $ Y $ \c0 -> let (x,c1) = m c0 in (unY . unZ) (f x) c1 -- Pace, too-strict puritans instance MonadState String (Z a) where get = Z $ Y $ \c -> (show c, c) put x = Z $ Y $ \_ -> ((), read x)
So far so good. Now for the Symantics instances (abridged).
class Symantics repr where int :: Int -> repr Int -- int literal add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (a->b)
instance Symantics (Y String) where int = unZ . return . show add x y = unZ $ do sx <- Z x sy <- Z y return $ "(" ++ sx ++ " + " ++ sy ++ ")"
The add function illustrates the kind of do-sugaring we know and love that I want to use for Symantics.
lam f = unZ $ do show_c0 <- get let vname = "v" ++ show_c0 c0 = read show_c0 :: VarCount c1 = succ c0 fz :: Z a String -> Z b String fz = Z . f . unZ put (show c1) s <- (fz . return) vname return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"
Now with lam, I get this cryptic error message (under 6.8.2): Occurs check: cannot construct the infinite type: b = a -> b When trying to generalise the type inferred for `lam' Signature type: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) Type to generalise: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) In the instance declaration for `Symantics (Y String)' Both the two types in the error message are identical, which suggests no generalization is needed. I'm puzzled why ghc sees an infinite type. Any ideas on how to proceed? -- View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagle... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
Kim-Ee Yeoh wrote:
The add function illustrates the kind of do-sugaring we know and love that I want to use for Symantics.
lam f = unZ $ do show_c0 <- get let vname = "v" ++ show_c0 c0 = read show_c0 :: VarCount c1 = succ c0 fz :: Z a String -> Z b String fz = Z . f . unZ put (show c1) s <- (fz . return) vname return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"
Now with lam, I get this cryptic error message (under 6.8.2):
Occurs check: cannot construct the infinite type: b = a -> b When trying to generalise the type inferred for `lam' Signature type: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) Type to generalise: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) In the instance declaration for `Symantics (Y String)'
Both the two types in the error message are identical, which suggests no generalization is needed. I'm puzzled why ghc sees an infinite type.
Any ideas on how to proceed?
Not an answer, but just a different error message from GHC 6.10.3 when I tried loading up your code. kyagrd@kyavaio:~/tmp$ ghci EvalTaglessF.hs GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Main ( EvalTaglessF.hs, interpreted ) EvalTaglessF.hs:264:14: Couldn't match expected type `b1' against inferred type `b' `b1' is a rigid type variable bound by the type signature for `fz' at EvalTaglessF.hs:263:31 `b' is a rigid type variable bound by the type signature for `lam' at EvalTaglessF.hs:248:26 Expected type: Z b1 String Inferred type: Z b String In the expression: Z . f . unZ In the definition of `fz': fz = Z . f . unZ EvalTaglessF.hs:264:22: Couldn't match expected type `a1' against inferred type `a' `a1' is a rigid type variable bound by the type signature for `fz' at EvalTaglessF.hs:263:17 `a' is a rigid type variable bound by the type signature for `lam' at EvalTaglessF.hs:248:16 Expected type: Z a1 String Inferred type: Z a String In the second argument of `(.)', namely `unZ' In the second argument of `(.)', namely `f . unZ' Failed, modules loaded: none. I hope this gives you a hint, if any. I am not exactly sure about how to solve this but I might try using scoped type variables extension somehow if I were in your shoe.
Actually the problem lies in your definition of fz, it has the wrong type to be used in lam. The Z you get out of fz as type Z b String, but you need it to have Z (a -> b) String so that when you strip off the Z you have a Y String (a -> b) matching the result type of lam. To get there replace your definition of fz with:
fz :: Z a String -> Z (a -> b) String fz = Z . Y . unY . f . unZ
In 6.10.2 I used {-# LANGUAGE FlexibleInstances, TypeSynonymInstances,
MultiParamTypeClasses, ScopedTypeVariables #-}
and that compiled just fine.
On Thu, Jul 2, 2009 at 8:02 PM, Ahn, Ki Yung
Kim-Ee Yeoh wrote:
The add function illustrates the kind of do-sugaring we know and love that I want to use for Symantics.
lam f = unZ $ do
show_c0 <- get let vname = "v" ++ show_c0 c0 = read show_c0 :: VarCount c1 = succ c0 fz :: Z a String -> Z b String fz = Z . f . unZ put (show c1) s <- (fz . return) vname return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"
Now with lam, I get this cryptic error message (under 6.8.2):
Occurs check: cannot construct the infinite type: b = a -> b When trying to generalise the type inferred for `lam' Signature type: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) Type to generalise: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) In the instance declaration for `Symantics (Y String)'
Both the two types in the error message are identical, which suggests no generalization is needed. I'm puzzled why ghc sees an infinite type.
Any ideas on how to proceed?
Not an answer, but just a different error message from GHC 6.10.3 when I tried loading up your code.
kyagrd@kyavaio:~/tmp$ ghci EvalTaglessF.hs GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Main ( EvalTaglessF.hs, interpreted )
EvalTaglessF.hs:264:14: Couldn't match expected type `b1' against inferred type `b' `b1' is a rigid type variable bound by the type signature for `fz' at EvalTaglessF.hs:263:31 `b' is a rigid type variable bound by the type signature for `lam' at EvalTaglessF.hs:248:26 Expected type: Z b1 String Inferred type: Z b String In the expression: Z . f . unZ In the definition of `fz': fz = Z . f . unZ
EvalTaglessF.hs:264:22: Couldn't match expected type `a1' against inferred type `a' `a1' is a rigid type variable bound by the type signature for `fz' at EvalTaglessF.hs:263:17 `a' is a rigid type variable bound by the type signature for `lam' at EvalTaglessF.hs:248:16 Expected type: Z a1 String Inferred type: Z a String In the second argument of `(.)', namely `unZ' In the second argument of `(.)', namely `f . unZ' Failed, modules loaded: none.
I hope this gives you a hint, if any. I am not exactly sure about how to solve this but I might try using scoped type variables extension somehow if I were in your shoe.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Edward Kmett 쓴 글:
Actually the problem lies in your definition of fz, it has the wrong type to be used in lam.
The Z you get out of fz as type Z b String, but you need it to have Z (a -> b) String so that when you strip off the Z you have a Y String (a -> b) matching the result type of lam.
To get there replace your definition of fz with:
fz :: Z a String -> Z (a -> b) String fz = Z . Y . unY . f . unZ
I think this seems to be the Yeoh wanted. Mine was just blinded hack just to make it type check without looking at what program means.
I don't know if this is what you want but I was at least able to make it to type check basically changing (fz . return) into simply return. I think the error message about the occurs check was because of the fz function is used wrong (or you didn't give it a correct type).
You might also look at doing it without all the State monad noise with something like:
class Symantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (a->b) app :: repr (a -> b) -> repr a -> repr b
newtype Pretty a = Pretty { runPretty :: [String] -> String }
pretty :: Pretty a -> String pretty (Pretty f) = f vars where vars = [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ]
instance Symantics Pretty where int = Pretty . const . show add x y = Pretty $ \vars -> "(" ++ runPretty x vars ++ " + " ++ runPretty y vars ++ ")" lam f = Pretty $ \ (v:vars) -> "(\\" ++ v ++ ". " ++ runPretty (f (var v)) vars ++ ")" where var = Pretty . const app f x = Pretty $ \vars -> "(" ++ runPretty f vars ++ " " ++ runPretty x vars ++ ")"
-Edward Kmett
On Thu, Jul 2, 2009 at 5:52 PM, Kim-Ee Yeoh
I'm trying to write HOAS Show instances for the finally-tagless type-classes using actual State monads.
The original code: http://okmij.org/ftp/Computation/FLOLAC/EvalTaglessF.hs
Two type variables are needed: one to vary over the Symantics class (but only as a phantom type) and another to vary over the Monad class. Hence, the use of 2-variable type constructors.
type VarCount = int newtype Y b a = Y {unY :: VarCount -> (b, VarCount)}
Not knowing of a type-level 'flip', I resort to newtype isomorphisms:
newtype Z a b = Z {unZ :: Y b a} instance Monad (Z a) where return x = Z $ Y $ \c -> (x,c) (Z (Y m)) >>= f = Z $ Y $ \c0 -> let (x,c1) = m c0 in (unY . unZ) (f x) c1 -- Pace, too-strict puritans instance MonadState String (Z a) where get = Z $ Y $ \c -> (show c, c) put x = Z $ Y $ \_ -> ((), read x)
So far so good. Now for the Symantics instances (abridged).
class Symantics repr where int :: Int -> repr Int -- int literal add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (a->b)
instance Symantics (Y String) where int = unZ . return . show add x y = unZ $ do sx <- Z x sy <- Z y return $ "(" ++ sx ++ " + " ++ sy ++ ")"
The add function illustrates the kind of do-sugaring we know and love that I want to use for Symantics.
lam f = unZ $ do show_c0 <- get let vname = "v" ++ show_c0 c0 = read show_c0 :: VarCount c1 = succ c0 fz :: Z a String -> Z b String fz = Z . f . unZ put (show c1) s <- (fz . return) vname return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"
Now with lam, I get this cryptic error message (under 6.8.2):
Occurs check: cannot construct the infinite type: b = a -> b When trying to generalise the type inferred for `lam' Signature type: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) Type to generalise: forall a1 b1. (Y String a1 -> Y String b1) -> Y String (a1 -> b1) In the instance declaration for `Symantics (Y String)'
Both the two types in the error message are identical, which suggests no generalization is needed. I'm puzzled why ghc sees an infinite type.
Any ideas on how to proceed?
-- View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagle... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi Edward, Your runPretty version fits the bill nicely, thank you. I might still retain the state monad version because it allows generalizations beyond pretty-printing. As for fixing the original bug, I've found that the real magic lies in the incantation (Y . unY) inserted at the appropriate places. Indeed, I've removed type signatures because try as I might, I couldn't write something the type-checker would accept. This is for 6.8.2. FWIW, the final version: instance Symantics (Y String) where int = unZ . return . show bool = unZ . return . show lam f = unZ $ do show_c0 <- get let vname = "v" ++ show_c0 c0 = read show_c0 :: VarCount c1 = succ c0 put (show c1) bodyf <- (Z . Y . unY . f . unZ . return) vname return $ "(\\" ++ vname ++ " -> " ++ bodyf ++ ")" fix f = pr3 [MkZa $ lam f] ["(fix ", ")"] app e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," " ,")"] add e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," + " ,")"] mul e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," * " ,")"] leq e1 e2 = pr3 [MkZa e1,MkZa e2] ["("," <= ",")"] if_ be et ee = pr3 [MkZa be,MkZa et,MkZa ee] ["(if "," then "," else ",")"] -- Suppress the Symantics phantom type by casting to an existential data Za where MkZa :: Y String a -> Za pr3 a b = unZ $ pr2 a b pr2 :: forall a. [Za] -> [String] -> Z a String pr2 _ [] = return "" pr2 [] ts = (return . concat) ts pr2 ((MkZa e):es) (t:ts) = do s1 <- (Z . Y . unY) e -- that (Y . unY) magical incantation again! s2 <- pr2 es ts return $ t ++ s1 ++ s2 Edward Kmett wrote:
You might also look at doing it without all the State monad noise with something like:
class Symantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (a->b) app :: repr (a -> b) -> repr a -> repr b
newtype Pretty a = Pretty { runPretty :: [String] -> String }
pretty :: Pretty a -> String pretty (Pretty f) = f vars where vars = [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ]
instance Symantics Pretty where int = Pretty . const . show add x y = Pretty $ \vars -> "(" ++ runPretty x vars ++ " + " ++ runPretty y vars ++ ")" lam f = Pretty $ \ (v:vars) -> "(\\" ++ v ++ ". " ++ runPretty (f (var v)) vars ++ ")" where var = Pretty . const app f x = Pretty $ \vars -> "(" ++ runPretty f vars ++ " " ++ runPretty x vars ++ ")"
-- View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagle... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
Kim-Ee Yeoh wrote:
type VarCount = int newtype Y b a = Y {unY :: VarCount -> (b, VarCount)}
Hi Edward,
Your runPretty version fits the bill nicely, thank you. I might still retain the state monad version because it allows generalizations beyond pretty-printing.
As for fixing the original bug, I've found that the real magic lies in the incantation (Y . unY) inserted at the appropriate places.
Aka unsafeCoerce, changing the phantom type |a|. The need to do it is caused by wanting to erase the existential introduced by Za/MkZa. Depending on what the phantom type is supposed to represent, this may or may not give the semantics/safety you're after. -- Live well, ~wren
Kim-Ee Yeoh wrote:
As for fixing the original bug, I've found that the real magic lies in the incantation (Y . unY) inserted at the appropriate places.
Aka unsafeCoerce, changing the phantom type |a|.
The type of (Y . unY) is (Y . unY) :: forall a b c. Y c a -> Y c b so modulo (Y c), it is indeed unsafeCoerce.
The need to do it is caused by wanting to erase the existential introduced by Za/MkZa.
That's not the primary reason. The earlier version of the code in my original message doesn't use existentials. We still however, need to "wobble" the type via (Y . unY) in order to typecheck.
Depending on what the phantom type is supposed to represent, this may or may not give the semantics/safety you're after.
If you're referring to the safety of the object/target language, then even without any Symantics instances, only type-correct code can compile, thanks to the finally-tagless embedding that "lifts" type-checking in the meta-language (Haskell) into type-checking for the target language. That safety isn't in the least bit compromised. The pretty-printing Symantics instance in question actually type-checks fine without unsafeCoerce or its like when written out without the additional Monad type-class abstraction and Y-Z isomorphism. Translating to the latter was entirely straightforward. Thanks to all who responded. -- View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagle... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
participants (4)
-
Ahn, Ki Yung -
Edward Kmett -
Kim-Ee Yeoh -
wren ng thornton