Following 48h Scheme Haskell Tutorial - Heterogeneous List & Existential types

Help
#1

Hey there!

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 :slight_smile:

In the tutorial they implement some weak typing check through heterogeneous lists.

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 Exists & 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

2 Likes
#2

I THINK something like this could work, obviously untested:

newtype Unpacker = AnyUnpacker (∀ r. (∀ a. Eq a => (LispVal -> ThrowsError a) -> r) -> r)

anyunpackernum = AnyUnpacker (\f -> f unpackNum)

unpackEquals :: LispVal -> LispVal -> Unpacker -> ThrowsError Boolean
unpackEquals arg1 arg2 (AnyUnpacker proof)
  = proof \unpacker -> do
      unpacked1 <- unpacker arg1
      unpacked2 <- unpacker arg2
      pure $ unpacked1 == unpacked2
    `catchError` (const $ pure false)

I’m not sure where that catchError is actually being parsed into, but it could go inside the \unpacker -> ... or outside, as by that point the type no longer contains a

2 Likes
#3

Damn, I think I see what’s going on a bit. Well, before anything, thanks a bunch. I think I get why the unpacker function needs to be in the inner most parens.

Seems to compile, I’ll have to see about that catchError placement. Also this looks like works:

anyUnpacker :: ∀ a. Eq a => (LispVal -> ThrowsError a) -> Unpacker
anyUnpacker unpacker = AnyUnpacker (_ $ unpacker)

A couple more of these and I’ll be an expert :))