CODEWITHSUNDEEP
haskelltypesfunctional-dependenciestype-families
emi
emi

Reputation: 5410

Functional Dependencies / Type Families - AST

I was recently introduced to functional dependencies and type families. For a class project I wrote (completed) an interpreter for a subset of C in Java and Haskell. The Haskell implementation of an evaluation function for terms required building "function tables" with explicit pattern matching and unwrapping of value constructors representing literals. An unhappy situation (but much prettier than the Java).

After searching for a while, I came across the "collections" example, wondering if I could apply this to my abstract syntax to produce generic "inject to" and "project from" functions for literals. I came up with two initial test attempts:

(Using functional dependencies: the injection and projection functions work without explicit type annotations, as does injection into Lit with lit. However, the projection function from Lit will not type, giving the error "couldn't match expected type l against inferred type l'".)

class Prim l a | l -> a, a -> l where
 inj  :: a -> l
 proj :: l -> a

instance Prim LB Bool where inj = LB; proj = lb
instance Prim LI Int  where inj = LI; proj = li

data LB = LB {lb :: Bool}
data LI = LI {li :: Int}

data E where Lit :: Prim l a => l -> E

lit :: Prim l a => l -> E
lit = Lit

unlit :: Prim l a => E -> l
unlit (Lit a) = a

(Using type families. The problem here is that I can't get Haskell to infer from an argument the correct return type without explicit annotation, and I can't write the generic functions lit :: Val l -> E and unlit :: E -> Val l.)

class Show l => Prim l where
 type Val l :: *
 inj  :: Val l -> l
 proj :: l -> Val l

data LB a = LB {lb :: Bool}
data LI a = LI {li :: Int }

instance Prim (LB a) where type Val (LB a) = Bool; inj = LB; proj = lb
instance Prim (LI a) where type Val (LI a) = Int;  inj = LI; proj = li;

data E where
 Lit :: Prim l => l -> E
 Bin :: Op -> E -> E -> E

I don't understanding type families well, and have a flimsy grasp on functional dependencies. But I'd like to know two things: (a) if the functions I want can be typed and implemented; (b) If I am misunderstanding something fundamental here. It almost works, but I've been fighting with the type checker for a while now.

EDIT This is a simple model of what I want, since it was unclear. The class Bin implements the functionality I want, basically. But I can't collect the various "wrappable and unwrappable" values together to make an AST out of this.

class L t l => Bin t l where
 bAp :: (t -> t -> t) -> l -> l -> l
 bAp f l r = inj (proj l `f` proj r)

class Show l => L t l | t -> l, l -> t where
  inj  :: t -> l
  proj :: l -> t
  typ  :: l -> T

instance Bin Int LI
instance Bin Bool LB

instance L Int  LI where inj = LI; proj = li; typ = const TI
instance L Bool LB where inj = LB; proj = lb; typ = const TB

data LI = LI {li :: Int}  deriving (Eq, Show)
data LB = LB {lb :: Bool} deriving (Eq, Show)

data T = TI | TB | TC | TF | TU deriving (Eq, Show)

Upvotes: 2

Views: 618

Answers (2)

ony
ony

Reputation: 13223

If you still want to stick with idea of polymorphic E. You can use polymorphic functions:

withUnlit :: E -> (forall l . Prim l => l -> b) -> b
withUnlit (Lit a) f = f a

But the only thing you can do (with traits you've given to Prim l) is:

showE :: E -> String
showE e = withUnlit e show

And inj and proj. But you have no way to work with Val l except of using some Data.Dynamic (if that is what I think).

Upvotes: 1

Heatsink
Heatsink

Reputation: 7751

The way you have defined the Lit constructor will prevent you from projecting out the value it contains, regardless of how you define the projection function.

Let's look at the constructor's type:

Lit :: Prim l => l -> E

The type variable l appears in the parameters, but not the return type. That means that when you construct a Lit, you put in a value of some type that's a member of Prim and then permanently forget what its type was.

I'm not sure how you want to eliminate pattern matching and unwrapping of value constructors. You basically have two choices for how to do projections:

  1. Project values at run time, using pattern matching or something equivalent to it.
  2. Project values at compile time, by proving using the type system that the data type you have is equal to the data type you want.

There are reasons to go with compile-time proofs, but it doesn't look like you have any of those reasons.

Upvotes: 4

Related Questions