Is it possible to write this function in Haskell?

Question

I study dependent types: in Haskell, I defined a canonical type

data Vec ∷ Type → Nat → Type where Nil ∷ Vec a Z (:-) ∷ a → Vec an → 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 an → Vec a (??) 

since the length of the result is unknown. I found it in Agda, and it 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 understood delete correctly, it was defined with the restriction x , which is an element of xs , in this case you simply delete 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 that is not currently available in Haskell. That is, the part (x : A)(xs : Vec A (suc n)) → ... not directly expressed. You can probably cook something using singletones, but it will be very ugly and complicated.

I would just define

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

and be alright with him. I would also reorder the arguments to Vec to provide Applicative , Traversable and other instances.

---

No, actually. To determine delete , you just need to specify the index 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 na where Nil :: Vec Z a (:-) :: a -> Vec na -> Vec (S n) a delete :: Index n -> Vec (S n) a -> Vec na 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 rich typed index.

---

Here is a single point solution:

 {-# 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 bxy where If True xy = x If False xy = 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 '[SZ, S (S (SZ)), Z] Nat test = delete (SS (SS SZ)) (SS SZ :- SS (SS (SS SZ)) :- SS (SS SZ) :- SZ :- Nil) 

Here we index Vec lists of their elements and save singletones as vector elements. We also define SEq , which is a type of class that contains a method that receives two singleton and returns either a proof of the equality of the values ​​they promote, or their inequality. Then we define the delete type family, which is similar to regular delete for lists, but at the type level. Finally, in the actual delete we map the pattern by x === y and, thus, show whether x y is equal or not, which forces us to calculate the type family.