I’ve been following the 48h Scheme Haskell Tutorial to get more mileage and I’ve come across an impediment related to the existential types… again
They do this by creating this data type:
data Unpacker = forall a. Eq a => AnyUnpacker (LispVal -> ThrowsError a)
I tried a bunch of things, including
TypeEquals, least of which:
newtype Unpacker = AnyUnpacker (∀ r. (∀ a. Eq a => a -> r) -> LispVal -> ThrowsError r)
Now… this almost works, but the problem is that he proof requires the result
r before applying the unpacker function (
LispVal -> ThrowsError r) if I understand right so that doesn’t work.
I mean it could work if we knew the type of
r and so we could do something like
unpacker (const 0) arg1 or
unpacker (const "") arg1 in:
unpackEquals :: LispVal -> LispVal -> Unpacker -> ThrowsError Boolean unpackEquals arg1 arg2 (AnyUnpacker unpacker) = do unpacked1 <- unpacker arg1 unpacked2 <- unpacker arg2 pure $ unpacked1 == unpacked2 pure false `catchError` (const $ pure false)
Which is the direct translation of the original Haskell code.
Other relevant info might be that:
type ThrowsError = Either LispError. I’m getting closer to understanding these existential types, it’s just that I don’t know how to provide the proofs with these nested types.
The idea is to create a heterogeneous list like:
[AnyUnpacker unpackNum, AnyUnpacker unpackStr, AnyUnpacker unpackBool] where
unpackNum :: LispVal -> ThrowsError Int and so on for the rest, with appropriate return types. This is just copy/paste from the tutorial, this works in Haskell.
Any ideas much appreciated! Thanks