Sigma.hs

{-# language TypeInType, GADTs, TemplateHaskell, ExistentialQuantification,
TypeApplications, TypeFamilies, TypeOperators, StandaloneDeriving, FlexibleContexts,
RankNTypes #-}

import Data.Kind
import Data.Singletons
import Data.Singletons.TH

data Sigma a f = forall (x :: a). Sigma (Sing x) (Apply f x)

withSigma :: Sigma a f -> (forall (x :: a). Sing x -> Apply f x -> r) -> r
withSigma (Sigma a f) g = g a f

data Nat = Z | S Nat
genSingletons [''Nat]

data Vect :: Nat -> Type -> Type where
  Nil :: Vect 'Z a
  Cons :: a -> Vect n a -> Vect ('S n) a
deriving instance Show a => Show (Vect n a)
deriving instance Eq a => Eq (Vect n a)

type SomeVect a n = Vect n a
data SomeVectSym0 :: Type ~> (Nat ~> Type)
data SomeVectSym1 (a :: Type) :: Nat ~> Type
type instance Apply SomeVectSym0 (a :: Type) = SomeVectSym1 a
type instance Apply (SomeVectSym1 a) (n :: Nat) = SomeVect a n

test :: Sigma Nat (Apply SomeVectSym0 Int)
test = Sigma (SS $ SS SZ) (Cons 1 (Cons 2 Nil))

filter' :: (a -> Bool) -> Vect n a -> Sigma Nat (Apply SomeVectSym0 a)
filter' _ Nil = Sigma SZ Nil
filter' pred (Cons a rest)
  | pred a =
      case filter' pred rest of
        Sigma ev val -> Sigma (SS ev) (Cons a val)
  | otherwise = filter' pred rest