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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
