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

[Günther Schmidt]

Hi Jacques,

thank you again for your post, better late than never :)!

Let me first apologize to you, I did not immediately recognize you as one  
of the authors of the "Finally Tagless" paper.


After 2 years now of using haskell at a mere layman's level and  
nevertheless writing better and more concise code than in the 10 years  
before using other languages I was ready to move a step further.


I must admit that things like type arithmetic, monads, functors and  
whathaveyou can be quite intimidating, but the other day I wrote my first  
monad, and it really wasn't that hard at all.


Anyway, so I had managed to improve my code slightly by introducing an  
abstraction, a tiny, trivial, naive DSL. That certainly was an eye-opener.


When you gave me your solution, I realized that while it was correct, that  
just couldn't be the last word on it. Something from Oleg that contains a  
bug? Can't be, I must have a mistake in my thinking here. So I didn't give  
up on "Finally Tagless" but read everything I could get my hands on, plus  
the responses to my posts were also quite enlightening.


One minor problem with your paper, and other work from Oleg, well to me  
that is, I don't ML. Also Oleg is such an "insider" sometimes he forgets  
tiny hints for the rest of us. The initial post (not from me) was about  
"An issue with finally tagless ..." and in Olegs response to that he  
eliminates the problem with ease (I know, typically Oleg). Well as soon as  
I tried that nothing worked until I put the "NoImplicitPrelude" in there,  
duh.


So at least now I know what to do next:

Design an EDSL taglessly for relational algebra (using HList too)
write one or 2 interpreters / compilers for SQL and in-memory
Dump the code I have written so far and pretend I never had.


Best wishes

Günther





Am 15.10.2009, 17:05 Uhr, schrieb Jacques Carette :


(sorry for the slow reply on this topic...)

Robert Atkey and Oleg presented some very interesting code in response  
to your query.  But some of you might (and should!) be asking "why on  
earth did Jacques use unsafePerformIO?", especially when neither Robert  
nor Oleg did.


Simply put: I answered your question exactly as asked, while they  
answered the question you *should* have asked.  At the exact 'type'  
involved in your question, there is no good answer; if you want an  
instance of lam at a monadic type 'directly', you need to 'extract' from  
the monad.  But the point is that that isn't really the right question.   
Rather than requiring complete parametric polymorphism in the  
answer-type, if you allow a little non-uniformity through a simple type  
family, the shift in types is sufficient to no longer require a monadic  
'extract' at all.


But even once you've gotten to that point, that's not enough, because at  
that point you still have the issue of what calling convention (by  
value, name or need) to use.  And figuring that out is rather fun, so  
you got detailed answer from Robert and Oleg explaining that part in  
detail.  Robert carefully used IntT and :-> to label the different  
types, and Oleg's code (http://okmij.org/ftp/tagless-final/CB.hs) showed  
how these were really just 'labels', which are useful mnemonics for  
humans, but not essential.


If you dig into our JFP paper describing "finally tagless" in all its  
gory details, you'll see that we use a poor man's version of type  
families there too (see section 4.3). Jacques





___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Jacques Carette]

(sorry for the slow reply on this topic...)

Robert Atkey and Oleg presented some very interesting code in response 
to your query.  But some of you might (and should!) be asking "why on 
earth did Jacques use unsafePerformIO?", especially when neither Robert 
nor Oleg did.


Simply put: I answered your question exactly as asked, while they 
answered the question you *should* have asked.  At the exact 'type' 
involved in your question, there is no good answer; if you want an 
instance of lam at a monadic type 'directly', you need to 'extract' from 
the monad.  But the point is that that isn't really the right question.  
Rather than requiring complete parametric polymorphism in the 
answer-type, if you allow a little non-uniformity through a simple type 
family, the shift in types is sufficient to no longer require a monadic 
'extract' at all.


But even once you've gotten to that point, that's not enough, because at 
that point you still have the issue of what calling convention (by 
value, name or need) to use.  And figuring that out is rather fun, so 
you got detailed answer from Robert and Oleg explaining that part in 
detail.  Robert carefully used IntT and :-> to label the different 
types, and Oleg's code (http://okmij.org/ftp/tagless-final/CB.hs) showed 
how these were really just 'labels', which are useful mnemonics for 
humans, but not essential.


If you dig into our JFP paper describing "finally tagless" in all its 
gory details, you'll see that we use a poor man's version of type 
families there too (see section 4.3). 


Jacques


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Robert Atkey]

On Mon, 2009-10-05 at 22:42 +0100, Robert Atkey wrote:

> There is a difference in the syntax between CBN and CBV that is not
> always obvious from the usual paper presentations. There is a split
> between pieces of syntax that are "values" and those that are
> "computations". Values do not have side-effects, while computations may.
> In this presentation, I have chosen that the only values are variables,
> while everything else is a computation.
> 

I should correct this: it is possible to give the CBV semantics to the
original syntax definition (with the single parameter in the type
class), you just have to move the "return" of the monad into the "lam"
case. I implied in the paragraph above that the split between values and
computations was required for CBV case; this is not true.

Bob


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Robert Atkey]

On Mon, 2009-10-05 at 19:22 -0400, David Menendez wrote:
> > The two obvious options are
> > call-by-name and call-by-value.
> 
> I wonder how easily one can provide both, like in Algol.

Fairly easy, you can either do a language that has an explicit monad (a
bit like Haskell with only the IO monad), or you can go the whole hog
and embed Paul Levy's Call-by-push-value. This requires a bit more
cleverness, and an explicit representation of the embedded types in
order to define the algebra maps on the computation types.

> Obviously, doing a deterministic version is simpler. You can probably
> get away with representing values as simple self-evaluating thunks.
> 
> data Thunk s a = STRef s (Either a (ST s a))
> 
> evalThunk :: Thunk s a -> ST s a
> evalThunk r = readSTRef r >>= either return update
> where
> update m = m >>= \x -> writeSTRef r (Left x) >> return x

I had a go at this and it seems to work. Happily, it is a tiny tweak to
the CBV implementation I gave: you just replace "return" with your
"evalThunk" (or something like it) and wrap the argument in the 'app'
case with a function that creates a thunk.

Bob



-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[David Menendez]

2009/10/5 Robert Atkey :
> Hi Günther,
>
> The underlying problem with the implementation of 'lam' is that
> you have to pick an evaluation order for the side effects you want in
> the semantics of your embedded language. The two obvious options are
> call-by-name and call-by-value.

I wonder how easily one can provide both, like in Algol.


> The other obvious evaluation strategy is call-by-need, as used by
> Haskell itself, but I don't know if it is possible to implement this. I
> guess it may be possible using the ST monad as the mutable storage of
> thunks.

Perhaps something along the lines of "Purely Functional Lazy
Non-deterministic Programming"?



Obviously, doing a deterministic version is simpler. You can probably
get away with representing values as simple self-evaluating thunks.

data Thunk s a = STRef s (Either a (ST s a))

evalThunk :: Thunk s a -> ST s a
evalThunk r = readSTRef r >>= either return update
where
update m = m >>= \x -> writeSTRef r (Left x) >> return x

-- 
Dave Menendez 

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Robert Atkey]

Hi Günther,

The underlying problem with the implementation of 'lam' is that 
you have to pick an evaluation order for the side effects you want in
the semantics of your embedded language. The two obvious options are
call-by-name and call-by-value.

The tricky point is that the types of the embedded language cannot be
interpreted directly as Haskell types wrapped in a monad. You need to 
either take the call-by-name or the call-by-value interpretation of
types:

For CBN:  [[ Int]] = IO Int
  [[ A -> B ]] = [[ A ]] -> [[ B ]]

For CBV:  [[ Int]] = Int
  [[ A -> B ]] = [[ A ]] -> IO [[ B ]]

(obviously, there is nothing special about the IO monad here, or in the
rest of this email: we could replace it with any other monad).

To implement the translation of embedded language types to Haskell types
in Haskell we use type families.

Here is the code for call-by-name:

> module CBN where

First of all, we define some dummy types so that we have a different
representation of types in the embedded language than those in the
meta-language, and we don't get confused:

> data IntT
> data a :-> b
> infixr 5 :->

Now we give the definition of the higher-order abstract syntax of our
embedded language:

> class HOAS exp where
> lam :: (exp a -> exp b) -> exp (a :-> b)
> app :: exp (a :-> b) -> exp a -> exp b
>
> int :: Int -> exp IntT
> add :: exp IntT -> exp IntT -> exp IntT

This is as in your definition, except I have used the different type
names to highlight the distinction between embedded and meta-language
types.

Next, we give the CBN semantics for the types, using the definition
above, with a type family.

> type family Sem a :: *
> type instance Sem IntT  = IO Int
> type instance Sem (a :-> b) = Sem a -> Sem b

Now we can give an instance of the syntax's type class, that translates
a piece of embedded code into its denotational semantics.

> newtype S a = S { unS :: Sem a }

> instance HOAS S where
>   int = S . return
>   add (S x) (S y) = S $ do a <- x
>b <- y
>putStrLn "Adding"
>return (a + b)
>
>   lam f   = S (unS . f . S)
>   app (S x) (S y) = S (x y)

As an example, we can give a term and see what happens when we evaluate
it:

> let_ :: HOAS exp => exp a -> (exp a -> exp b) -> exp b
> let_ x y = (lam y) `app` x

> t :: HOAS exp => exp IntT
> t = (lam $ \x -> let_ (x `add` x)
  $ \y -> y `add` y) `app` int 10

Evaluating 'unS t' in GHCi gives the output:

Adding
Adding
Adding
40

Note that the add operation is invoked three times: the "x `add` x" that
is let-bound is evaluated twice.



The second option is call-by-value. This is a bit more interesting
because we have to change the syntax of the embedded language to deal
with the different substitution rules for CBV.

> module CBV where

Again, we use a different representation for embedded-language types:

> data IntT
> data a :-> b
> infixr 5 :->

There is a difference in the syntax between CBN and CBV that is not
always obvious from the usual paper presentations. There is a split
between pieces of syntax that are "values" and those that are
"computations". Values do not have side-effects, while computations may.
In this presentation, I have chosen that the only values are variables,
while everything else is a computation.

To represent this split, we use a multi-parameter type class. Note that
the technique of using multi-parameter type classes is generally useful
for representing abstract syntaxes in the HOAS style with multiple
mutually defined syntactic categories.

> class HOAS exp val | exp -> val, val -> exp where
>val :: val a -> exp a
>
>lam :: (val a -> exp b) -> exp (a :-> b)
>app :: exp (a :-> b) -> exp a -> exp b
>
>int :: Int -> exp IntT
>add :: exp IntT -> exp IntT -> exp IntT

The 'val' operation injects values into computations: this will be
interpreted by the 'return' of the monad.

We now give the semantics of types for CBV, following the definition
above:

> type family   Sem a :: *
> type instance Sem IntT  = Int
> type instance Sem (a :-> b) = Sem a -> IO (Sem b)

We need two newtypes for the two different syntactic categories. Values
are interpeted by 'SV', and are just pure values; computations are
interpreted by wrapping them in the monad.

> newtype SV a = SV { unSV :: Sem a }
> newtype SC a = SC { unSC :: IO (Sem a) }

Now we can define the semantics of the syntax in terms of these types:

> instance HOAS SC SV where
> val = SC . return . unSV
>
> lam f = SC $ return (unSC . f . SV) 
> app (SC x) (SC y) = SC $ do f <- x; a <- y; f a
> 
> int i = SC $ return i
> add (SC x) (SC y) = SC $ do a <- x
> b <- y
> putStrLn "Adding"
> return (a + b)

The same example term is expressed in CBV as follows:

> let_ ::

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

[Jacques Carette]

BTW, here is a more symmetric version of the same code:
   lam f = I . return $ unsafePerformIO . unI . f . I . return

which has a very clear pattern of
 lam f = embed $ extract . f. embed

where 'embed' is often called "return".  Implementations of lam in 
"tagless final" style tend to follow the above pattern of embed/extract, 
each specialized to the particular repr implementation. 

In some cases, one only needs a "context-sensitive" extract, i.e. an 
extract which is only valid in the context of an outer 'embed'.  The 
most important example is code-generation in metaocaml where the 
'compiler' version of lam reads

 let lam f = . .~(f ..)>.
where the .~ does an extract -- but *only* in the context of a 
surrounding code bracket (i.e. .< >. ). 

If there is such a context-sensitive "extract" for the IO monad, i.e. 
something which allows you to pretend you've got a result in IO only 
valid *inside* IO, then you can use that to write a nicer lam. 

I tried all the obvious things with monadic operators to get this done, 
but did not succeed in the time I had.  Maybe Oleg or Ken can.  So don't 
give up hope quite yet!


Jacques

Günther Schmidt wrote:

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 :

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


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [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 :

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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Jacques Carette]

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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe