Có thể viết chức năng này trong Haskell không?

Question

tôi đang học loại phụ thuộc: Trong Haskell tôi đã xác định các loại kinh điển

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

và thực hiện hầu hết các chức năng từ Data.List tuy nhiên tôi không biết làm thế nào để viết, nếu có thể ở tất cả, các chức năng như

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

vì độ dài của kết quả không được xác định. Tôi đã tìm thấy nó trong Agda và nó thực hiện theo cách

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 

này Nếu tôi hiểu đúng delete nó được định nghĩa với Constrain của x là một phần tử của xs, trong trường hợp đó bạn chỉ cần loại bỏ x và trừ 1 từ chiều dài. Tôi có thể viết một cái gì đó như thế này trong Haskell?

Answer 1

Vấn đề là bạn cần một định lượng phụ thuộc mà Haskell hiện thiếu. I E. phần (x : A)(xs : Vec A (suc n)) → ... không thể hiển thị trực tiếp. Bạn có lẽ có thể nấu một thứ gì đó bằng cách sử dụng đơn, nhưng nó sẽ thực sự xấu xí và phức tạp.

Tôi chỉ sẽ xác định

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

và chịu tốt với nó. Tôi cũng sẽ thay đổi thứ tự của các đối số thành Vec để có thể cung cấp Applicative, Traversable và các trường hợp khác.

---

Thực ra, không. Để xác định delete bạn chỉ cần cung cấp một chỉ số mà tại đó để xóa:

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

Lưu ý rằng x ∈ xs là gì khác hơn là một chỉ số đa dạng gõ.

---

Đây là một giải pháp với độc thân:

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

Ở đây chúng ta chỉ Vec s bởi danh sách các yếu tố của họ và lưu trữ độc thân như các yếu tố của vectơ. Chúng tôi cũng định nghĩa SEq là một lớp kiểu có chứa một phương thức nhận hai đơn và trả về một bằng chứng về sự bình đẳng của các giá trị mà chúng thúc đẩy hoặc bất bình đẳng của chúng. Tiếp theo, chúng tôi định nghĩa họ loại Delete giống như thông thường delete cho danh sách, nhưng ở cấp loại. Cuối cùng trong delete thực tế, chúng tôi khớp mẫu trên x === y và do đó tiết lộ liệu x có bằng y hay không, điều này làm cho tính toán gia đình loại.