[Haskell-cafe] checking types with type families

[Evan Laforge]

I have a parameterized data type:

> data Val result = VNum Double | VThunk (SomeMonad result)
> type Environ result = Map Symbol (Val result)

I have a class to make it easier to typecheck Vals:

> class Typecheck a where
>   from_val :: Val result -> Maybe a
>
> instance Typecheck Double where
>   from_val (VNum d) = Just d
>   from_val _ = Nothing

Now I can write

> lookup_environ :: (Typecheck a) => Symbol -> Environ result -> Maybe a

Now of course there's a question of how to write Typecheck for VThunk.
 I would like to be able to call 'lookup_environ' expecting a
'SomeMonad result' and get Nothing or Just depending on if it's
present.

> instance Typecheck (SomeMonad result) where
>  from_val (VThunk f) = Just f

But I need something to say that the 'result' from the instance head
is the same as the 'result' from the class declaration, because
otherwise I get

Couldn't match expected type `result'
           against inferred type `result1'

So maybe a type family?

> class Typecheck ...
>   type ResultOf a :: *
>   from_val :: Val (ResultOf a) -> Maybe a
>
> instance Typecheck (SomeMonad result) where
>   type ResultOf (SomeMonad result) = result
> ...

Now the question is, what's the ResultOf a Double?  Well, since the
output doesn't depend on 'result' at all, I would like to be able to
write 'type ResultOf Double = anything', and then I can look up a VNum
in an 'Environ anything'.  Unfortunately, that type declaration isn't
legal because it wants 'anything' to be bound somewhere.  I tried
explicitly introducing 'anything' with a forall, but no dice.

So there are a number of possible solutions to this problem.  One is,
is there another way to get from the expression language type VNum,
VThunk, etc. to a haskell type that doesn't use typeclasses in this
way?

Or, is there a way to assert in the instance of 'Typecheck (SomeMonad
result)' that its 'result' is equal to the 'result' in the class
declaration without using type families in this way?

Or, is there a way to use type families in the way I'm using them to
leave 'result' polymorphic in the cases where it can be left free in
the result (e.g. VNum 42 :: Val anything)?

I know lots of people have used haskell to write little interpreters,
so maybe someone has solved this problem before.  Basically, I have a
Val that is "semi-polymorphic", but even if I go the totally
monomorphic / dynamic type route by making a Result type with all the
different types, I still have trouble converting from haskell types
and back when I need to write the "Result -> result" function.  I
suppose I could play the same Typecheck game there, but I like the
idea of an "Environ X" that doesn't admit the wrong kind of VThunk.
It seems like I should be able to express that in the type system and
be safer as well as save some packing and unpacking.