Is it possible to write this function in Haskell?

Question

I'm learning dependent types: In Haskell I have defined the canonical type

data Vec ∷ Type → Nat → Type where
  Nil  ∷ Vec a Z
  (:-) ∷ a → Vec a n → Vec a (S n)

and implemented most of the functions from Data.List however I don't know how to write, if possible at all, functions like

delete ∷ Eq a ⇒ a → Vec a n → Vec a (??)

since the length of the result is not known. I have found it in Agda and it's implemented this way

delete : {A : Set}{n : Nat}(x : A)(xs : Vec A (suc n)) → x ∈ xs → Vec A n
delete           .x (x ∷ xs)  hd    = xs
delete {A}{zero } _  ._      (tl ())
delete {A}{suc _} y (x ∷ xs) (tl p) = x ∷ delete y xs p

If I understand correctly delete it's defined with the constrain of x being an element of xs, in that case you just remove x and subtract 1 from the length. Can I write something like this in Haskell?

Answer 1

The problem is that you need a dependent quantifier which Haskell currently lacks. I.e. the (x : A)(xs : Vec A (suc n)) → ... part is not directly expressible. You can probably cook up something using singletons, but it'll be really ugly and complicated.

I would just define

delete ∷ Eq a ⇒ a → Vec a (S n) → Maybe (Vec a n)

and be fine with it. I'd also change the order of arguments to Vec to make it possible to provide Applicative, Traversable and other instances.

---

Actually, no. In order to define delete you just need to provide an index at which to delete:

{-# LANGUAGE GADTs, DataKinds #-}

data Nat = Z | S Nat

data Index n where
  IZ :: Index n
  IS :: Index n -> Index (S n)

data Vec n a where
  Nil  :: Vec Z a
  (:-) :: a -> Vec n a -> Vec (S n) a

delete :: Index n -> Vec (S n) a -> Vec n a
delete  IZ    (x :-  xs)       = xs
delete (IS n) (x :- (y :- xs)) = x :- delete n (y :- xs)

Note that x ∈ xs is nothing more than a richly typed index.

---

Here is a solution with singletons:

{-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, UndecidableInstances, TypeFamilies, RankNTypes, TypeOperators #-}

infixr 5 :-

data Nat = Z | S Nat

data family Sing (x :: a)

data instance Sing (b :: Bool) where
  STrue  :: Sing True
  SFalse :: Sing False

data instance Sing (n :: Nat) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)

type family (:==) (x :: a) (y :: a) :: Bool

class SEq a where
  (===) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x :== y)

type instance Z   :== Z   = True
type instance S n :== Z   = False
type instance Z   :== S m = False
type instance S n :== S m = n :== m

instance SEq Nat where
  SZ   === SZ   = STrue
  SS n === SZ   = SFalse
  SZ   === SS m = SFalse
  SS n === SS m = n === m

data Vec xs a where
  Nil  :: Vec '[] a
  (:-) :: Sing x -> Vec xs a -> Vec (x ': xs) a

type family If b x y where
  If True  x y = x
  If False x y = y

type family Delete x xs where
  Delete x  '[]      = '[]
  Delete x (y ': xs) = If (x :== y) xs (y ': Delete x xs)

delete :: forall (x :: a) xs. SEq a => Sing x -> Vec xs a -> Vec (Delete x xs) a
delete x  Nil      = Nil
delete x (y :- xs) = case x === y of
  STrue  -> xs
  SFalse -> y :- delete x xs

test :: Vec '[S Z, S (S (S Z)), Z] Nat
test = delete (SS (SS SZ)) (SS SZ :- SS (SS (SS SZ)) :- SS (SS SZ) :- SZ :- Nil)

Here we index Vecs by lists of their elements and store singletons as elements of vectors. We also define SEq which is a type class that contains a method that receives two singletons and returns either a proof of equality of values they promote or their inequality. Next we define a type family Delete that is like usual delete for lists, but at the type level. Finally in the actual delete we pattern match on x === y and thus reveal whether x is equal to y or not, which makes the type family compute.