[Haskell-cafe] problem implementing an EDSL in Haskell

[Daniil Elovkov]

Hello folks

Haskell is considered good for embedded DSLs. I'm trying to implement
some simple EDSL in a typeful manner and having a problem with looking
up variable values.

I've got an Expression GADT, which admits variables. The problem is
with writing compute function which will lookup variable values in a
type-safe manner.

The exp. data type is like this

data Exp a where
   Const a :: Val a -> Exp a
   Var :: a -> String -> Exp a -- where the first comp. isn't
used,only for type info.
   ....

So, obviously, I have to perform lookups in some 'scope' to compute
the expression. By scope I mean the list of (name,value) pairs.

How do I represent the scope? Well, I haven't gone that far as to
encode statically the information about the type of every variable in
scope. Instead, I used existentials to hide their types and put'em all
in a list.

For that purpose I introduced pack/unpack.

-- value with dynamic type annotation
-- m here and below can be Val, Exp, etc.
--     to represent Val Int, Exp Int, etc.
data Type m = TInt (m Int)  | TString (m String) | TDouble (m Double)

class Typed a where
    typ   :: m a -> Type m

instance Typed Int where typ x = TInt x
instance Typed String where typ x = TString x
instance Typed Double where typ x = TDouble x

data Opaque m = forall a. (Typed a) => Opaque (m a)

-- extract to an annotated representation
extract :: Opaque m -> Type m
extract (Opaque a) = typ a

How would you suggest, I write compute function?

My try was

compute :: Scope -> Exp t -> Val t
compute scope (Const x) = x -- trivial

compute scope (Var t name) = -- intereseting part
    let opq = lookup name scope
        val = case opq of
                Nothing  -> error "not in scope"
                Just opq -> extract opq
        expType   = aux t
    in case val `matches` expType of -- I'd like to make some 'matches' func.
        Nothing -> error "type error" -- which would either produce an error
        Just v  -> v     -- or return the value, based on run-time tags

matches :: Typed m -> Typed m -> Maybe (m a)
  BUT of course this type is bad, there's no 'a' in the left side
matches (TInt x) (TInt _) = Just x
matches (TString x) (TString _) = Just x
matches (TDouble x) (TDouble _) = Just x
matches _ _                     = Nothing

So, clearly the problem is in that Type m has no evidence of a, which
was its very purpose. Ok, so I made

data FType m a where
    FInt :: m Int -> FType m Int
    FString :: m String -> FType m String
    FDouble :: m Double -> Aux m a

class Typed a where
    typ   :: m a -> Type m -- as before
    ftyp :: m a -> FType m a -- new one

and again obvious instance
instance Typed Int where ftyp x = FInt x
...

And of course, I'd like to get that information somehow
           extract2 (Opaque a) = ftyp a
I rewrote 'matches' accordingly but the problem is already in the type
of extract2

its type Opaque m -> (forall a. (Typed a) => m a)
is not good to ghc, less polymorphic than expected

So, in principle it must be doable, since opaque data retains its
dictionary, and by that I can get a dynamic tag, say FInt x, where x
is proved to be Int.

What would you suggest?

Thank you