Возможно ли записать эту функцию в Haskell?

Question

Я изучаю зависимые типы: В Haskell я определил канонический тип

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

и реализовано большинство функций из Data.List однако я не знаю, как писать, если вообще возможно, функции как

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

поскольку длина результата неизвестна. Я нашел его в Agda и он реализован таким образом

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 

Если я правильно понял delete он определен с Constrain из x является элементом xs, в этом случае вы просто удалить x и вычесть 1 из длины. Могу ли я написать что-то подобное в Haskell?

Answer 1

Проблема в том, что вам нужен зависимый квантор, который в настоящее время отсутствует в Haskell. То есть часть (x : A)(xs : Vec A (suc n)) → ... прямо не выражается. Вы, вероятно, можете приготовить что-то, используя одиночные игры, но это будет очень уродливо и сложно.

Я бы просто определить

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

и хорошо с ним. Я также изменил бы порядок аргументов на Vec, чтобы предоставить Applicative, Traversable и другие экземпляры.

---

Собственно, нет. Для того чтобы определить 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) 

Обратите внимание, что x ∈ xs является не более чем богато типизированным индекс.

---

Вот решение с одноплодной:

{-# 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) 

Здесь индекс Vec s по спискам их элементов и хранить одиночек в качестве элементов векторов. Мы также определяем SEq, который является типом класса, который содержит метод, который получает два синглтона и возвращает либо доказательство равенства ценностей, которые они продвигают, либо их неравенство. Затем мы определяем семейство типов Delete, которое, как обычно, delete для списков, но на уровне типа. Наконец, в фактическом delete мы сопоставляем шаблон по x === y и таким образом показываем, равен ли xy или нет, что делает вычисление семейства типов.