[Haskell-cafe] Scrap your rolls/unrolls
Max Bolingbroke
batterseapower at hotmail.com
Wed Nov 3 05:24:04 EDT 2010
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
More information about the Haskell-Cafe
mailing list