Existential types in idris

existentials.idr

module Main

import Data.Vect

exists : {k : Type} -> (k -> Type) -> Type
exists t = (b : Type) -> ({a : _} -> t a -> b) -> b

packExists : {k : Type} -> {t : k -> Type} -> {a : k} -> t a -> exists t
packExists x = \b, f => f x

unpackExists : {k : Type} -> {t : k -> Type} -> exists t -> {b : Type} -> ({a : k} -> t a -> b) -> b
unpackExists exT {b = b'} f = exT b' f

-- Specialised versions of the above existential for length-indexed vectors

SomeVect : Type -> Type
SomeVect a = exists (\n => Vect n a)

wrapVector : Vect n a -> SomeVect a
wrapVector v = packExists {t = \n => Vect n a} v

-- I prefer the "with" notation as it makes it explicit that you require some
-- extra function to access the existential
unwrapVectorWith : {a, b : Type} -> ({n : Nat} -> Vect n a -> b) -> SomeVect a -> b
unwrapVectorWith {a = a'} f vect = unpackExists {t = \n => Vect n a'} vect f


-- Examples of usage

cons : a -> SomeVect a -> SomeVect a
cons x sv = unwrapVectorWith (\xv => wrapVector (x :: xv)) sv

vectFromList : List a -> SomeVect a
vectFromList Nil = wrapVector Nil
vectFromList (x::xs) = cons x (vectFromList xs)


-- Obviously we can just as easily sum a list, but pretend that there is some
-- operation over vectors we can't do directly over a list, then there may be
-- a more sensible reason for using an existential like this.

svSum : SomeVect Integer -> Integer
svSum sv = unwrapVectorWith sum sv

sumViaVect : List Integer -> Integer
sumViaVect xs = svSum $ vectFromList xs