Re: [Haskell-cafe] Scrap your rolls/unrolls

[Max Bolingbroke]

On 2 November 2010 14:10, Bertram Felgenhauer
bertram.felgenha...@googlemail.com wrote:
 Indeed. I had a lot of fun with the ideas of this thread, extending
 the 'Force' type family (which I call 'Eval' below) to a small EDSL
 on the type level:

I also came up with this.. I was trying to use it to get two type
classes for (Monoid Int) like this, but it doesn't work:


{-# LANGUAGE TypeFamilies, EmptyDataDecls, ScopedTypeVariables,
TypeOperators, FlexibleInstances, FlexibleContexts #-}

import Data.Monoid


-- Type family for evaluators on types
type family E a :: *

-- Tag for functor application: fundamental to our approach
infixr 9 :%
data f :% a

-- Tags for evalutor-style data declarations: such declarations
contain internal
-- occurrences of E, so we can delay evaluation of their arguments
data P0T (f :: *)
type instance E (P0T f) = f
data P1T (f :: * - *)
type instance E (P1T f :% a) = f a
data P2T (f :: * - * - *)
type instance E (P2T f :% a :% b) = f a b
data P3T (f :: * - * - * - *)
type instance E (P3T f :% a :% b :% c) = f a b c

-- When applying legacy data types we have to manually force the arguments:
data FunT
type instance E (FunT :% a :% b) = E a - E b
data Tup2T
type instance E (Tup2T :% a :% b) = (E a, E b)
data Tup3T
type instance E (Tup3T :% a :% b :% c) = (E a, E b, E c)


-- Evalutor-style versions of some type classes
class FunctorT f where
fmapT :: (E a - E b) - E (f :% a) - E (f :% b)

class MonoidT a where
memptyT :: E a
mappendT :: E a - E a - E a


data AdditiveIntT
type instance E AdditiveIntT = Int
instance MonoidT AdditiveIntT where
memptyT = 0
mappendT = (+)

data MultiplicativeIntT
type instance E MultiplicativeIntT = Int
instance MonoidT MultiplicativeIntT where
memptyT = 1
mappendT = (*)

-- Make the default instance of Monoid be additive:
instance MonoidT (P0T Int) where
memptyT = memptyT :: E AdditiveIntT
mappendT = mappendT :: E AdditiveIntT - E AdditiveIntT - E AdditiveIntT


main = do
print (result :: E (P0T Int))
print (result :: E MultiplicativeIntT)
  where
result :: forall a. (E a ~ Int, MonoidT a) = E a
result = memptyT `mappendT` 2 `mappendT` 3


The reason it doesn't work is clear: it is impossible to tell GHC
which MonoidT Int dictionary you intend to use, since E is not
injective! I think this is a fundamental flaw in the scheme.

 The implementation is somewhat verbose, but quite straight-forward
 tree manipulation.

This is impressively mad. You can eliminate phase 1 by introducing the
identity code (at least, it typechecks):


data Id
type instance Eval (App Id a) = Eval a



type instance Eval (Fix a) = Eval (Fix1 a Id)

data Fix1 a b
-- compositions, phase 2.: build left-associative composition
type instance Eval (Fix1 (a :.: (b :.: c)) d) = Eval (Fix1 ((a :.: b) :.: c) d)
type instance Eval (Fix1 (a :.: Id) c) = Eval (Fix1 a c)
type instance Eval (Fix1 (a :.: ConE b) c) = Eval (Fix1 a (ConE b :.: c))
type instance Eval (Fix1 (a :.: Con1 b) c) = Eval (Fix1 a (Con1 b :.: c))
-- compositions, final step: apply first element to fixpoint of shifted cycle
type instance Eval (Fix1 Id b) = Eval (Fix b)
type instance Eval (Fix1 (ConE a) b) = a (Fix (b :.: ConE a))
type instance Eval (Fix1 (Con1 a) b) = a (Eval (Fix (b :.: Con1 a)))


I'm not sure whether this formulation is clearer or not.

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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Bertram Felgenhauer]

Max Bolingbroke wrote:
 On 23 October 2010 15:32, Sjoerd Visscher sjo...@w3future.com wrote:
  A little prettier (the cata detour wasn't needed after all):
 
    data IdThunk a
    type instance Force (IdThunk a) = a
 
 Yes, this IdThunk is key - in my own implementation I called this Forced, 
 so:
 
 
 type instance Force (Forced a) = a
 
 
 You can generalise this trick to abstract over type functions, though
 I haven't had a need to do this yet. Let us suppose you had these
 definitions:
...
 With type functions, Haskell finally type-level lambda of a sort :-)

Indeed. I had a lot of fun with the ideas of this thread, extending
the 'Force' type family (which I call 'Eval' below) to a small EDSL
on the type level:

The EDSL supports constants

  data Con (t :: *)-- type constant
  data Con1 (t :: * - *)  -- unary type constructor
  data ConE (t :: * - *)  -- like Con1, but the argument is used with Eval

and a few operators

  data App a b -- apply a to b
  data Fix a   -- compute fixpoint of a
  data a :.: b -- compose two unary type constructors

There is a type family Eval that maps expressions from that EDSL to
actual types,

  type family Eval t :: *

The basic operations are straight-forward to implement,

  type instance Eval (Con t) = t
  type instance Eval (App (Con1 t) a) = t (Eval a)
  type instance Eval (App (ConE t) a) = t a
  type instance Eval (App (a :.: b) c) = Eval (App a (App b c))

Now we turn to fixed points. An easy definition would be

  type instance Eval (Fix f) = Eval (App f (Fix f))

Let's play with that. For that, we defined

  data TreeF a t = Node a [Eval t]
  type Tree a = Eval (Fix (ConE (TreeF a)))

  -- works fine in ghc 7.1
  -- ghc 6.12.3 chokes on it for the recursive types
  deriving instance (Show a, Show (Eval t)) = Show (TreeF a t)

And indeed,

  ghci Node 1 [Node 2 []] :: Tree Int
  Node 1 [Node 2 []]

and a lot of other things work as expected. But what if we want to
work with fixed points of the composition of several functors?

This works fine:

  type Tree2 a b = Eval (Fix (ConE (TreeF a) :.: ConE (TreeF b)))

  t0 :: Tree2 Bool Int
  t0 = Node True [Node 1 [Node False []]]

  t1 :: Tree2 Int Bool
  t1 = Node 1 [Node True [Node 1 [Node False [

but this doesn't:

  t1 :: Tree2 Int Bool
  t1 = Node 1 [t0]

We can help the type checker out by evaluating fixed points for
compositions differently: Instead of applying the whole sequence
of functors at once, apply them one by one, and keep the remaining
sequence in a nice shape so that the type checker can identify
equivalent compositions.

The implementation is somewhat verbose, but quite straight-forward
tree manipulation.

  -- easy case first
  type instance Eval (Fix (ConE f)) = f (Fix (ConE f))

  -- handle compositions, phase 1.: find last element.
  type instance Eval (Fix (a :.: (b :.: c))) = Eval (Fix ((a :.: b) :.: c))
  type instance Eval (Fix (a :.: (ConE b))) = Eval (Fix1 a (ConE b))
  type instance Eval (Fix (a :.: (Con1 b))) = Eval (Fix1 a (Con1 b))

  data Fix1 a b
  -- compositions, phase 2.: build left-associative composition chain
  type instance Eval (Fix1 (a :.: (b :.: c)) d) = Eval (Fix1 ((a :.: b) :.: c) 
d)
  type instance Eval (Fix1 (a :.: ConE b) c) = Eval (Fix1 a (ConE b :.: c))
  type instance Eval (Fix1 (a :.: Con1 b) c) = Eval (Fix1 a (Con1 b :.: c))

  -- compositions, final step: apply first element to fixpoint of shifted cycle
  type instance Eval (Fix1 (ConE a) b) = a (Fix (b :.: ConE a))
  type instance Eval (Fix1 (Con1 a) b) = a (Eval (Fix (b :.: Con1 a)))

And with that implementation, the above definition of  t1  typechecks.

Full code with more examples is available at

  http://int-e.cohomology.org/~bf3/haskell/Fix.hs

Best regards,

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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Sebastian Fischer]

Hi Max,

neat idea! Haskell supports laziness even on the type level ;)

I tried to play with your code but did not get very far. I quickly ran  
into two problems.


On Oct 22, 2010, at 7:37 PM, Max Bolingbroke wrote:


The annoying part of this exercise is the the presence of a Force in
the functor definition (e.g ListF) means that you can't make them into
actual Functor instances! The fmap definition gives you a function of
type (a - b) and you need one of type (Force a - Force b). However,
you can make them into a category-extras:Control.Functor.QFunctor
instance


I think `Control.Functor.Categorical.CFunctor` is a more natural  
replacement for functor here. One can define


instance CFunctor (ListF a) ForceCat Hask

and I was hoping that I could define `fold` based on CFunctor but I  
did not succeed. The usual definition of `fold` is


fold :: Functor f = (f a - a) - Fix f - a
fold f = f . fmap (fold f)

and I tried to replace this with

fold :: CFunctor f ForceCat Hask = ...

but did not find a combination of type signature and definition that  
compiled.


My second problem came up when writing a `Show` instance for the  
`List` type. This works:


instance Show a = Show (List a) where
  show Nil = Nil
  show (Cons x xs) = (Cons  ++ show x ++   ++ show xs ++ )

But trying to avoid TypeSynonymInstances leads to a non-terminating  
`show` function:


instance (Show a, Show (Force rec)) = Show (ListF a rec) where
  show Nil = Nil
  show (Cons x xs) = (Cons  ++ show x ++   ++ show xs ++ )

Shouldn't both work?

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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Sjoerd Visscher]

On Oct 23, 2010, at 1:27 PM, Sebastian Fischer wrote:
 
 I think `Control.Functor.Categorical.CFunctor` is a more natural replacement 
 for functor here. One can define
 
instance CFunctor (ListF a) ForceCat Hask
 
 and I was hoping that I could define `fold` based on CFunctor but I did not 
 succeed. The usual definition of `fold` is
 
fold :: Functor f = (f a - a) - Fix f - a
fold f = f . fmap (fold f)
 
 and I tried to replace this with
 
fold :: CFunctor f ForceCat Hask = ...
 
 but did not find a combination of type signature and definition that compiled.

The catamorphism lies in the ForceCat category. Also, you can't just pass a 
to f because Force a is undefined.

   data IdThunk a
   type instance Force (IdThunk a) = a

   cata :: CFunctor f ForceCat (-) = (f (IdThunk a) - a) - ForceCat 
(FixThunk f) (IdThunk a)
   cata alg = ForceCat $ alg . cmap (cata alg)

Then you can define fold as follows:

   fold :: CFunctor f ForceCat (-) = (f (IdThunk a) - a) - Fix f - a
   fold = unForceCat . cata

Fortunately the IdThunk does not get in the way when defining algebras:

   sumAlg :: ListF Int (IdThunk Int) - Int
   sumAlg Nil = 0
   sumAlg (Cons a r) = a + r

greetings,
Sjoerd Visscher




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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Sjoerd Visscher]

A little prettier (the cata detour wasn't needed after all):

   data IdThunk a
   type instance Force (IdThunk a) = a
   type Alg f a = f (IdThunk a) - a

   fold :: CFunctor f ForceCat (-) = Alg f a - Fix f - a
   fold alg = alg . cmap (ForceCat $ fold alg)

   sumAlg :: Alg (ListF Int) Int
   sumAlg Nil = 0
   sumAlg (Cons a r) = a + r

   sumList :: List Int - Int
   sumList = fold sumAlg

It all works out very well, so this trick seems to be really useful!

Sjoerd

On Oct 23, 2010, at 4:05 PM, Sjoerd Visscher wrote:

 
 On Oct 23, 2010, at 1:27 PM, Sebastian Fischer wrote:
 
 I think `Control.Functor.Categorical.CFunctor` is a more natural replacement 
 for functor here. One can define
 
   instance CFunctor (ListF a) ForceCat Hask
 
 and I was hoping that I could define `fold` based on CFunctor but I did not 
 succeed. The usual definition of `fold` is
 
   fold :: Functor f = (f a - a) - Fix f - a
   fold f = f . fmap (fold f)
 
 and I tried to replace this with
 
   fold :: CFunctor f ForceCat Hask = ...
 
 but did not find a combination of type signature and definition that 
 compiled.
 
 The catamorphism lies in the ForceCat category. Also, you can't just pass a 
 to f because Force a is undefined.
 
   data IdThunk a
   type instance Force (IdThunk a) = a
 
   cata :: CFunctor f ForceCat (-) = (f (IdThunk a) - a) - ForceCat 
 (FixThunk f) (IdThunk a)
   cata alg = ForceCat $ alg . cmap (cata alg)
 
 Then you can define fold as follows:
 
   fold :: CFunctor f ForceCat (-) = (f (IdThunk a) - a) - Fix f - a
   fold = unForceCat . cata
 
 Fortunately the IdThunk does not get in the way when defining algebras:
 
   sumAlg :: ListF Int (IdThunk Int) - Int
   sumAlg Nil = 0
   sumAlg (Cons a r) = a + r
 
 greetings,
 Sjoerd Visscher
 
 
 
 
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe
 

--
Sjoerd Visscher
http://w3future.com




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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Max Bolingbroke]

On 23 October 2010 15:32, Sjoerd Visscher sjo...@w3future.com wrote:
 A little prettier (the cata detour wasn't needed after all):

   data IdThunk a
   type instance Force (IdThunk a) = a

Yes, this IdThunk is key - in my own implementation I called this Forced, so:


type instance Force (Forced a) = a


You can generalise this trick to abstract over type functions, though
I haven't had a need to do this yet. Let us suppose you had these
definitions:


{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}

type family Foo a :: *
type instance Foo Int = Bool
type instance Foo Bool = Int

type family Bar a :: *
type instance Bar Int = Char
type instance Bar Bool = Char


Now you want to build a data type where you have abstracted over the
particular type family to apply:


data GenericContainer f_clo = GC (f_clo Int) (f_clo Bool)
type FooContainer = GenericContainer Foo
type BarContainer = GenericContainer Bar


This is a very natural thing to do, but it is rejected by GHC because
Foo and Bar are partially applied in FooContainer and BarContainer.
You can work around this by eta expanding Foo/Bar using a newtype,
but it is more elegant to scrap your newtype injections/extractions
with the trick:


data FooClosure
data BarClosure


type family Apply f a :: *
type instance Apply FooClosure a = Foo a
type instance Apply BarClosure a = Bar a


data GenericContainer f_clo = GC (Apply f_clo Int) (Apply f_clo Bool)
type FooContainer = GenericContainer FooClosure
type BarContainer = GenericContainer BarClosure


These definitions typecheck perfectly:


valid1 :: FooContainer
valid1 = GC True 1

valid2 :: BarContainer
valid2 = GC 'a' 'b'


With type functions, Haskell finally type-level lambda of a sort :-)

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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Sjoerd Visscher]

I use Apply for Functor application in data-category, I used an infix operator 
:%

http://hackage.haskell.org/packages/archive/data-category/0.3.0.1/doc/html/src/Data-Category-Functor.html#line-57

F.e. composition is defined like this:

type instance (g :.: h) :% a = g :% (h :% a)

Sjoerd

On Oct 23, 2010, at 6:07 PM, Max Bolingbroke wrote:

 On 23 October 2010 15:32, Sjoerd Visscher sjo...@w3future.com wrote:
 A little prettier (the cata detour wasn't needed after all):
 
   data IdThunk a
   type instance Force (IdThunk a) = a
 
 Yes, this IdThunk is key - in my own implementation I called this Forced, 
 so:
 
 
 type instance Force (Forced a) = a
 
 
 You can generalise this trick to abstract over type functions, though
 I haven't had a need to do this yet. Let us suppose you had these
 definitions:
 
 
 {-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
 
 type family Foo a :: *
 type instance Foo Int = Bool
 type instance Foo Bool = Int
 
 type family Bar a :: *
 type instance Bar Int = Char
 type instance Bar Bool = Char
 
 
 Now you want to build a data type where you have abstracted over the
 particular type family to apply:
 
 
 data GenericContainer f_clo = GC (f_clo Int) (f_clo Bool)
 type FooContainer = GenericContainer Foo
 type BarContainer = GenericContainer Bar
 
 
 This is a very natural thing to do, but it is rejected by GHC because
 Foo and Bar are partially applied in FooContainer and BarContainer.
 You can work around this by eta expanding Foo/Bar using a newtype,
 but it is more elegant to scrap your newtype injections/extractions
 with the trick:
 
 
 data FooClosure
 data BarClosure
 
 
 type family Apply f a :: *
 type instance Apply FooClosure a = Foo a
 type instance Apply BarClosure a = Bar a
 
 
 data GenericContainer f_clo = GC (Apply f_clo Int) (Apply f_clo Bool)
 type FooContainer = GenericContainer FooClosure
 type BarContainer = GenericContainer BarClosure
 
 
 These definitions typecheck perfectly:
 
 
 valid1 :: FooContainer
 valid1 = GC True 1
 
 valid2 :: BarContainer
 valid2 = GC 'a' 'b'
 
 
 With type functions, Haskell finally type-level lambda of a sort :-)
 
 Cheers,
 Max
 





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

[Haskell-cafe] Scrap your rolls/unrolls

[Max Bolingbroke]

Hi Cafe,

In generic programming, e.g. as in Data Types a la Carte and Compos,
you often wish to work with data types in their fix-point of a functor
form. For example:


data ListF a rec = Nil | Cons a rec
newtype List a = Roll { unroll :: ListF a (List a) }


In some presentations, this is done by factoring the fix point like so:


newtype FixF f = Roll { unroll :: f (FixF f) }
type List a = FixF (ListF a)


This is all well and good, but it means when working with data types
defined in this manner you have to write Roll and unroll everywhere.
This is tedious :-(

Something I have long wished for is equirecursion, which would let you
write this instead:


type List a = ListF a (List a)


Note that we now have a type instead of a newtype, so we won't need to
write any injection/extraction operators. However, currently GHC
rightly rejects this with a complaint about a cycle in type synonym
declarations.

However, you can use type families to hide the cycle from GHC:


type List a = ListF a (Force (ListThunk a))
data ListThunk a
type family Force a
type instance Force (ListThunk a) = List a


Unfortunately, this requires UndecidableInstances (the type instance
RHS is not smaller than the instance head). And indeed when we turn
that extension on, GHC goes into a loop, so this may not seem very
useful.

However, we can make this slight modification to the data type to make
things work again:


data ListF a rec = Nil | Cons a (Force rec)
type List a = ListF a (ListThunk a)


Note that the application of Force has moved into the *use site* of
rec rather than the *application site*. This now requires no
extensions other than TypeFamilies, and the client code of the library
is beautiful (i.e. has no rolls/unrolls):


example, ones :: List Int
example = Cons 1 (Cons 2 Nil)
ones = Cons 1 ones


We can factor this trick into a fix point combinator that does not
require roll/unroll:


type Fix f = f (FixThunk f)
type List a = Fix (ListF a)
data FixThunk f
type family Force a
type instance Force (FixThunk f) = Fix f


The annoying part of this exercise is the the presence of a Force in
the functor definition (e.g ListF) means that you can't make them into
actual Functor instances! The fmap definition gives you a function of
type (a - b) and you need one of type (Force a - Force b). However,
you can make them into a category-extras:Control.Functor.QFunctor
instance 
(http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor.html)
by choosing the s Category to be:


newtype ForceCat a b = ForceCat { unForceCat :: Force a - Force b }

instance Category ForceCat where
  id = ForceCat id
  ForceCat f . ForceCat g = ForceCat (f . g)


Rather than the usual Hask Category which is used in the standard
Functor. This is somewhat unsatisfying, but I'm not sure there is a
better way.

I haven't seen this trick to emulate equirecursion before. Has it
showed up anywhere else?

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

Re: [Haskell-cafe] Scrap your rolls/unrolls

[Dan Doel]

On Friday 22 October 2010 6:37:49 am Max Bolingbroke wrote:
 This is all well and good, but it means when working with data types
 defined in this manner you have to write Roll and unroll everywhere.
 This is tedious :-(

Your discovery is interesting (and I haven't seen it before).

Another solution, though, is SHE. With it, you can write:

  data ListF a r = NilF | ConsF a r
  newtype List a = Roll (ListF a (List a))

  pattern Nil   = Roll NilF
  pattern Cons x xs = Roll (ConsF x xs)

And not worry about Rolls anymore.

-- Dan

http://personal.cis.strath.ac.uk/~conor/pub/she/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe