[Haskell-cafe] Scrap your rolls/unrolls

[Max Bolingbroke]

On 2 November 2010 14:10, Bertram Felgenhauer
<bertram.felgenhauer at 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