Projecting existential variables
https://richarde.dev/papers/2021/exists/exists.pdf shows how we can project existential variables, using the expressions themselves to "non-generatively" introduce special skolems, rather than be confined to pattern matching and getting fresh skolems confined to scopes. These "applicative skolems" (to continue to borrow the ML functor terminology), are a nice thing to have with or without exists a. ...
new "structural" existential types.
With lots of other hypothetical syntax:
data Foo where
MkFoo :: forall a. Show a => a :: Foo
_1 :: Foo -> Type -- but indicate non-relevant somehow?
_2 :: forall (a :: Foo) -> Dict (Show (fst a))
_3 :: forall (a :: Foo) -> fst a
foo :: Foo -> String
foo f = case _2 a of
Dict -> show x
where
type T = _1 a
x :: T = _3 a
_2
requires case
, but that is only because of Dict
. We could imagine explicit dictionary arguments or something instead, but that is separate.
The paper also goes into term-level constraints, which seems good for Dependent Haskell in general, but I suppose that should also have a separate issue.
CC @rae