Czy można napisać tę funkcję w Haskell?

Question

uczę typy zależne: W Haskell Mam zdefiniowane kanoniczny typ

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

i wdrożone większość funkcji z Data.List jednak nie wiem jak napisać, jeśli w ogóle możliwe, funkcje jak

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

, ponieważ długość wyniku nie jest znana. Znalazłem go w Agda i jest realizowany w ten sposób

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 

Jeśli dobrze rozumiem delete jest zdefiniowana z ograniczeniem od x będąc elementem xs, w tym przypadku po prostu usunąć x i odjąć 1 od długości. Czy mogę napisać coś takiego w Haskell?

Answer 1

Problem polega na tym, że potrzebujesz kwantyfikatora zależnego, którego Haskell aktualnie nie ma. To znaczy. część (x : A)(xs : Vec A (suc n)) → ... nie można bezpośrednio wyrazić. Możesz prawdopodobnie ugotować coś za pomocą singletonów, ale będzie to naprawdę brzydkie i skomplikowane.

Chciałbym po prostu zdefiniować

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

i być w porządku z nim. Zmieniłbym także kolejność argumentów na Vec, aby umożliwić dostarczenie Applicative, Traversable i innych instancji.

---

W rzeczywistości nie. W celu zdefiniowania delete wystarczy dostarczyć indeks, w którym do usunięcia:

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

Zauważ, że x ∈ xs jest niczym więcej niż bogato wpisany indeksu.

---

Oto rozwiązanie z pojedynczych:

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

Tutaj indeks Vec s wykazy ich elementów i przechowywania pojedynczych jako elementów wektorów. Definiujemy również SEq, która jest klasą typu, która zawiera metodę, która odbiera dwa singletony i zwraca albo dowód równości wartości, które promują, albo ich nierówność. Następnie definiujemy rodzinę typów Delete, która jest jak zwykle delete dla list, ale na poziomie typu. Wreszcie w rzeczywistości delete dopasowujemy wzór na x === y i tym samym ujawniamy, czy x jest równe czy nie, co powoduje, że rodzina typów jest obliczana.