Use of existentials

Question

I am reading through this excellent paper "Functional Programming with Structured Graphs, Bruno C. d. S. Oliveira" (some video here) and I'm trying to implement all the structures as I go. I'm struggling with the use of existentials. Although the author mentions Haskell throghout, it seems the types are more easily expressed in Coq or Agda. How can I make this compile? Thanks.

Code

data PStream a v = Var v
                 | Mu (v -> PStream a v)
                 | Cons a (PStream a v)

data Stream a = forall v. Pack {pop :: PStream a v} 


foldStream :: (a -> b -> b) -> b -> Stream a -> b
foldStream f k (Pack s) = pfoldStream s
    where pfoldStream (Var x)     = x
          pfoldStream (Mu g)      = pfoldStream (g k)
          pfoldStream (Cons x xs) = f x (pfoldStream xs)

Errors

error:
 Couldn't match type `v' with `b'
      `v' is a rigid type variable bound by
          a pattern with constructor
            Pack :: forall a v. PStream a v -> Stream a,
          in an equation for `foldStream'
          at C:\...\StructuredGraph.hs:17:17
      `b' is a rigid type variable bound by
          the type signature for
            foldStream :: (a -> b -> b) -> b -> Stream a -> b
          at C:\...\StructuredGraph.hs:17:1
    Expected type: PStream a b
      Actual type: PStream a v
    In the first argument of `pfoldStream', namely `s'
    In the expression: pfoldStream s

Answer 1

You have an existential type, but it looks like the type mentioned in the paper is universal (though I haven't read it beyond the definition of Stream).

There's a big difference between

newtype Stream a = forall v. Pack { pop :: PStream a v }

and

newtype Stream a = Pack { forall v. pop :: PStream a v }

The former doesn't seem very useful for this type, because you have no way of knowing what v is. The latter makes your code compile.