[Haskell-cafe] Finally tagless - stuck with implementation of "lam"

[Günther Schmidt]

Hello Jacques,

thanks, that is disappointing in some way, guess I still have a lot to  
learn.

Günther


Am 05.10.2009, 18:06 Uhr, schrieb Jacques Carette <carette at mcmaster.ca>:

> It's possible, but it's not nice.  You need to be able to "get out of  
> the monad" to make the types match, i.e.
>     lam f = I (return $ \x -> let y = I (return x) in
>                               unsafePerformIO $ unI (f y))
>
> The use of IO 'forces' lam to transform its effectful input into an even  
> more effectful result.  Actually, same goes for any monad used inside a  
> 'repr'.
>
> let_ and fix follow a similar pattern (although you can hide that  
> somewhat by re-using lam if you wish).
>
> Jacques
>
> Günther Schmidt wrote:
>> Hi all,
>>
>> I'm playing around with finally tagless.
>>
>> Here is the class for my Syntax:
>>
>>
>> class HOAS repr where
>>     lam :: (repr a -> repr b) -> repr (a -> b)
>>     app :: repr (a -> b) -> repr a -> repr b
>>     fix :: (repr a -> repr a) -> repr a
>>     let_ :: repr a -> (repr a -> repr b) -> repr b
>>
>>     int :: Int -> repr Int
>>     add :: repr Int -> repr Int -> repr Int
>>     sub :: repr Int -> repr Int -> repr Int
>>     mul :: repr Int -> repr Int -> repr Int
>>
>>
>> and here is one instance of that class for semantics.
>>
>>
>>
>> newtype I a = I { unI :: IO a }
>>
>> instance HOAS I where
>>     app e1 e2 = I (do
>>                     e1' <- unI e1
>>                     e2' <- unI e2
>>                     return $ e1' e2')
>>     int i = I (putStrLn ("setting an integer: " ++ show i) >> return i)
>>     add e1 e2 = I (do
>>                     e1' <- unI e1
>>                     e2' <- unI e2
>>                     putStrLn (printf "adding %d with %d" e1' e2')
>>                     return $ e1' + e2')
>>     sub e1 e2 = I (do
>>                     e1' <- unI e1
>>                     e2' <- unI e2
>>                     putStrLn (printf "subtracting %d from %d" e1' e2')
>>                     return $ e1' - e2')
>>     mul e1 e2 = I (do
>>                     e1' <- unI e1
>>                     e2' <- unI e2
>>                     putStrLn (printf "multiplying %d with %d" e1' e2')
>>                     return $ e1' * e2')
>>
>>
>> I'm stuck with the "lam" method, for 2 days now I've been trying to get  
>> it right, but failed.
>>
>> Is there a possibility that it isn't even possible?
>>
>> Günther
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>