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.