CODEWITHSUNDEEP
haskellgadt
Clinton
Clinton

Reputation: 23135

Library for existential type wrappers

Lets say I've got the following:

data T a

f :: a -> (exists t. T t)
g :: T b -> c

h :: a -> c
h = g . f

As I know, the type signature for f is not valid Haskell. I can instead do this though:

{-# LANGUAGE GADTs #-}

data T a

data ExistsTA where
  ExistsTA :: T a -> ExistsTA

f :: a -> ExistsTA
g :: T b -> c

h :: a -> c
h x = case (f x) of ExistsTA x' -> g x'

Which compiles fine. I was wondering, is there a library that generalises the creation of the ExistsTA data type (perhaps takes T as a parameter), or do I have to roll my own everytime I want to do this (which is not a big deal, just don't want to reinvent the wheel if I don't need too).

In particular, for my application, I would also like wrappers in this form:

data C where
  C1 :: C
  ...

data D (a :: C) where
  D1 a :: D
  ...

data T (d :: D) a

f :: T (D1 C1) a -> exists c. T (D1 c) a

Upvotes: 2

Views: 130

Answers (1)

Benjamin Hodgson
Benjamin Hodgson

Reputation: 44634

I dunno whether this is in a library anywhere, but I like to use the following general-purpose existential:

data Ex f = forall a. Ex (f a)

With PolyKinds Ex can existentially wrap up the parameter of any type f :: k -> *. How general-purpose is this? We can manipulate f until it's the right shape, and we can build in whatever extra information we need, with a little library of type combinators. Working with general-purpose types like this is a powerful way to program, but often it's simpler just to roll your own.

Suppose we want to existentially quantify both halves of a two-parameter type p. One can use the following GADT to uncurry p, turning it from a two-parameter type k1 -> k2 -> * into a one-parameter type (k1, k2) -> *.

data Uncurry p ij where
    Uncurry :: { getUncurry :: p i j } -> Uncurry p '(i, j)

Now Uncurry p can be existentially wrapped.

type ExP p = Ex (Uncurry p)

Suppose I want to pair up my existentially-wrapped type with some evidence such as a singleton, so that one can recover the existentially quantified index. I'll use the index-respecting product to pair up two functors f and g:

newtype (f :*: g) i = f i :*: g i

If, say, f is a GADT, pattern-matching on the f-half of the pair will tell you about g's index. Now, f :*: g has the right kind to be existentially wrapped.

type ExPair f g = Ex (f :*: g)

In practice you might write ExPair Sing f to pair up f with a singleton.

Suppose I need the aforementioned evidence in constraint form. I can replace Sing from above with the following type which reifies an instance dictionary for c a as a (visible) runtime value:

data Dict1 c a where
    Dict1 :: c a => Dict1 c a

(or you could use the constraints package: newtype Dict1 c a = Dict1 { getDict1 :: Dict (c a) }.) Now I just need to set the left-hand part of my pair to be Dict1 c:

type ExDictPair c f = ExPair (Dict1 c) f

So you might write ExDictPair SingI f to package up an implicit singleton.

Suppose the thing I need to existentially quantify is at a higher kind, eg * -> *. (I might want to talk about "some instance of Monad containing an Int".) Ex is poly-kinded, but it only existentially quantifies the right-most parameter of its argument. So we need the * -> * part of the type to be the last argument of our datatype. I can write a type combinator for that too:

newtype RApp a f = RApp { getRApp :: f a }

type SomeMonadAppliedToInt = ExDictPair Monad (RApp Int)

Upvotes: 3

Related Questions