matteo vezzola | 21 Mar 11:32 2013
Picon

Excercise on tagless final interpreters

I'm playing with tagless final interpreters reading [1], using a very simple language:

>>> class Ints repr where
>>>     int :: Integer -> repr Integer
>>>     (.+.) :: repr Integer -> repr Integer -> repr Integer
>>>     (.*.) :: repr Integer -> repr Integer -> repr Integer
>>>     (.-.) :: repr Integer -> repr Integer
>>>     (.<=.) :: repr Integer -> repr Integer -> repr Bool

>>> newtype P repr t = P { unP :: Bool -> repr t }
>>> instance Ints repr => Ints (P repr) where
>>>     int n = P $ \ s -> if s then int n else (.-.) (int n)
>>>     (.-.) n = P $ unP n . not
>>>     n .+. m = P $ \ s -> unP n s .+. unP m s
>>>     n .*. m = P $ \ s -> unP n s .*. unP m s
>>>     n .<=. m = P $ \ s -> unP n s .<=. unP m s

After pushing down negations I'd like to distribute (.*.) over (.+.). [1] leaves it as an exercise, so it
can't be that hard, but I don't get it...

Anyone knows how I could do it?

[1]: <http://okmij.org/ftp/tagless-final/course/lecture.pdf>

thanks,
--

-- 
matteo
Jacques Carette | 21 Mar 13:56 2013
Picon
Picon

Re: Excercise on tagless final interpreters

On 13-03-21 06:32 AM, matteo vezzola wrote:
> I'm playing with tagless final interpreters reading [1], using a very simple language:
>
>>>> class Ints repr where
>>>>      int :: Integer -> repr Integer
>>>>      (.+.) :: repr Integer -> repr Integer -> repr Integer
>>>>      (.*.) :: repr Integer -> repr Integer -> repr Integer
>>>>      (.-.) :: repr Integer -> repr Integer
>>>>      (.<=.) :: repr Integer -> repr Integer -> repr Bool
>>>> newtype P repr t = P { unP :: Bool -> repr t }
>>>> instance Ints repr => Ints (P repr) where
>>>>      int n = P $ \ s -> if s then int n else (.-.) (int n)
>>>>      (.-.) n = P $ unP n . not
>>>>      n .+. m = P $ \ s -> unP n s .+. unP m s
>>>>      n .*. m = P $ \ s -> unP n s .*. unP m s
>>>>      n .<=. m = P $ \ s -> unP n s .<=. unP m s
> After pushing down negations I'd like to distribute (.*.) over (.+.). [1] leaves it as an exercise, so it
can't be that hard, but I don't get it...
>
> Anyone knows how I could do it?
>
> [1]: <http://okmij.org/ftp/tagless-final/course/lecture.pdf>
>
>
> thanks,

It is exactly the same idea: you use a context to track whether you have 
something (a multiplication) waiting to be distributed.  It is a tad 
more involved because you need to track more than a single bit of 
information.
(Continue reading)

Brent Yorgey | 21 Mar 16:26 2013

Re: Excercise on tagless final interpreters

On Thu, Mar 21, 2013 at 11:32:21AM +0100, matteo vezzola wrote:
> I'm playing with tagless final interpreters reading [1], using a very simple language:
> 
> >>> class Ints repr where
> >>>     int :: Integer -> repr Integer
> >>>     (.+.) :: repr Integer -> repr Integer -> repr Integer
> >>>     (.*.) :: repr Integer -> repr Integer -> repr Integer
> >>>     (.-.) :: repr Integer -> repr Integer
> >>>     (.<=.) :: repr Integer -> repr Integer -> repr Bool
> 
> >>> newtype P repr t = P { unP :: Bool -> repr t }
> >>> instance Ints repr => Ints (P repr) where
> >>>     int n = P $ \ s -> if s then int n else (.-.) (int n)
> >>>     (.-.) n = P $ unP n . not
> >>>     n .+. m = P $ \ s -> unP n s .+. unP m s

> >>>     n .*. m = P $ \ s -> unP n s .*. unP m s
> >>>     n .<=. m = P $ \ s -> unP n s .<=. unP m s

Incidentally, these last two lines seem wrong.  It is not the case
that -(n*m) = (-n)*(-m) or that  n <= m  iff  (-n) <= (-m).

-Brent

Gmane