Tôi làm cách nào để thể hiện loại 'takeWhile for vectơ'?

Question

Người mới bắt đầu sử dụng Haskell tại đây. Tôi đã xác định các loại sau:

data Nat = Z | S Nat 
data Vector a n where 
    Nil :: Vector a Z 
    (:-) :: a -> Vector a n -> Vector a (S n) 
infixl 5 :- 

Tôi đang cố gắng viết hàm, takeWhileVector hoạt động giống như takeWhile trong danh sách, nhưng trên Vectors.

thực hiện của tôi là như sau:

takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 
takeWhileVector f Nil = Nil 
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil 

này không biên dịch và tạo ra các lỗi sau:

Could not deduce (m ~ 'S n0) 
from the context (n ~ 'S n1) 
    bound by a pattern with constructor 
      :- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n), 
      in an equation for ‘takeWhileVector’ 
    at takeWhileVector.hs:69:20-26 
    ‘m’ is a rigid type variable bound by 
     the type signature for 
     takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 
     at takeWhileVector.hs:67:20 
Expected type: Vector a m 
    Actual type: Vector a ('S n0) 
Relevant bindings include 
    takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 
    (bound at takeWhileVector.hs:69:1) 
In the expression: (x :- takeWhileVector f xs) 
In an equation for ‘takeWhileVector’: 
    takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs) 

Tôi đã có thể nghĩ rằng định nghĩa kiểu của tôi cho takeWhileVector nói như sau:

Đối với tất cả các loại 'a' và 'n của loại Nat, hàm này trả về' Vector a m ', trong đó' m 'là loại Nat.

Tôi có cần phải thay đổi chữ ký loại takeWhileVector để cụ thể hơn để nó cho thấy kết quả là Vector a (m :: Nat) không? Nếu không, làm cách nào tôi có thể thay đổi điều này để biên dịch?

Answer 1

Loại bạn đề nghị không thể được thực hiện, ví dụ: nó không phải là nơi sinh sống:

takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 

Hãy nhớ rằng người gọi chọn các biến kiểu a,n,m. Điều này có nghĩa là người gọi có thể sử dụng chức năng của bạn như ví dụ:

takeWhileVector :: (a -> Bool) -> Vector a Z -> Vector a (S Z) 

điều này là vô lý, vì bạn không thể tạo ra một số a nếu bạn không có gì lúc đầu. Thậm chí thực tế hơn, người gọi hàm này không có nghĩa là có thể chọn bao nhiêu kết quả để có và vượt qua một hàm hoàn toàn không liên quan - điều đó sẽ không đồng ý với ngữ nghĩa dự định của takeWhile.

Tôi đoán những gì bạn thực sự có nghĩa là một cái gì đó giống như

takeWhileVector :: (a -> Bool) -> Vector a n -> exists m. Vector a m 

trừ exists đó không phải là cú pháp Haskell hợp lệ. Thay vào đó, bạn cần một cái gì đó giống như

data SomeVector a where 
    S :: Vector a m -> SomeVector a 

takeWhileVector :: (a -> Bool) -> Vector a n -> SomeVector a 

Answer 2

Không có cách nào để tĩnh biết chiều dài của Vec được trả về bởi takeWhileVec: nó phụ thuộc vào các giá trị chứa trong Vec, và các chức năng bạn sử dụng. Tuy nhiên, những gì tôi có thể làm là cung cấp cho bạn một giá trị mà bạn có thể khớp mẫu trên tìm hiểu độ dài của Vec. Nhập singleton values.

data Natty n where 
    Zy :: Natty Z -- pronounced 'zeddy', because I'm a limey 
    Sy :: Natty n -> Natty (S n) -- pronounced 'essy' 

Đối với một trao n loại Nat, có đúng một (phi undefined) giá trị của loại Natty n. Vì vậy, nếu bạn biết điều gì đó về một số Natty, bạn cũng biết điều gì đó về loại cấp liên quan Nat. *

Tại sao chúng ta không thể sử dụng Nat cho mục đích này? Haskell duy trì sự tách biệt giữa các giá trị và loại.Loại cấp Nat không có liên quan, trừ một sự tương đồng về cấu trúc, với giá trị cấp Nat: giá trị S Z có một loại Nat, không S' Z' - vì vậy chúng ta phải sử dụng Natty, một bản sao thứ hai của Nat, tự buộc các giá trị và các loại với nhau. (Các hệ thống được đánh máy phụ thuộc thực như Agda cho phép bạn sử dụng lại cùng một số Nat cho cả tính toán mức giá trị và loại mức.)

_{* Bạn cũng có thể truyền bá kiến ​​thức theo cách khác.}

---

Kế hoạch này là để trả lại vector đầu ra cũng như chiều dài của nó như một Natty, với các loại sắp xếp theo một cách mà GHC hiểu rằng Natty không thực sự đại diện cho chiều dài của nó. Trước tiên, bạn có thể xem xét sự thay đổi này trên ví dụ trong câu hỏi của bạn:

-- takeWhile :: (a -> Bool) -> Vec a n -> (Natty m, Vec a m) 

Nhưng điều này không nói điều đúng: chúng ta đang nói takeWhile có thể trả lại bất kỳ m của sự lựa chọn của người gọi, đó là không đúng sự thật! Nó chỉ có thể trả về duy nhất m được xác định bởi hàm và vectơ đầu vào. Như tôi đã đề cập, điều này là không thể biết tại thời gian biên dịch, vì vậy chúng tôi phải giữ độ dài một bí mật từ trình biên dịch.

data AVec a = forall n. AVec (Natty n) (Vec a n) 

AVec là một existential type: n xuất hiện ở phía bên tay phải nhưng không phải bên trái. Kỹ thuật này cho phép bạn mô phỏng dependent pair type: loại của Vec phụ thuộc vào giá trị của Natty. Các cặp phụ thuộc rất hữu ích bất cứ khi nào các thuộc tính tĩnh của dữ liệu phụ thuộc vào thông tin động không có sẵn tại thời gian biên dịch.

Chúng tôi có thể viết takeWhile thẳng thắn bây giờ:

takeWhile :: (a -> Bool) -> Vec a n -> AVec a 
takeWhile f Nil = AVec Zy Nil 
takeWhile f (x :- xs) = case takeWhile f xs of 
          AVec n ys -> if f x 
              then AVec (Sy n) (x :- ys) 
              else AVec Zy Nil 

Chúng tôi phải ném kiến ​​thức đi tĩnh của chiều dài của Vector, vì vậy làm thế nào để bạn sử dụng một AVec với một chức năng mà đặt yêu cầu tĩnh vào độ dài? Do cách thức AVec được xây dựng, chúng tôi biết rằng Natty ở khe bên trái đại diện cho chiều dài của vectơ trong khe bên phải: cả hai đều có cùng thông số loại (tồn tại ẩn) n. Vì vậy, bằng cách khớp mẫu trên Natty, chúng tôi tìm hiểu độ dài của Vec.

head :: Vec a (S n) -> a 
head (x :- xs) = x 

head' :: AVec a -> Maybe a 
head' (AVec Zy Nil) = Nothing 
head' (AVec (Sy n) xs) = Just (head xs) 

Trong ví dụ này, chúng ta chỉ quan tâm liệu vector dài hơn một, vì vậy mô hình kết hợp trên Sy là đủ để chứng minh cho GHC rằng chúng ta nên được phép sử dụng head. (Xem a related answer of mine cho một ví dụ tham gia nhiều hơn của minh sự thật về AVec s.)

---

@chi đề cập đến một ý tưởng trêu ngươi: bạn có thể muốn để chứng minh rằng các vector được trả về bởi takeWhile không phải là dài hơn vector đầu vào.

takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n 

nơi AShorterVec là loại vector không quá n. Thách thức của chúng tôi là viết ra định nghĩa của AShorterVec.

Với hai số tự nhiên, làm thế nào bạn có thể chắc chắn rằng số đầu tiên nhỏ hơn hoặc bằng số thứ hai? Mối quan hệ là quy nạp. Nếu toán hạng bên trái bằng không, thì nó sẽ tự động nhỏ hơn hoặc bằng với bất kỳ số tự nhiên nào. Nếu không, một số sẽ nhỏ hơn hoặc bằng số khác nếu số tiền trước của nó nhỏ hơn hoặc bằng với tiền thân của người kia. Chúng ta có thể mã hóa nó như là một bằng chứng xây dựng bằng cách sử dụng một GADT.

data LTE n m where 
    ZLte :: LTE Z m 
    SLte :: LTE n m -> LTE (S n) (S m) 

Nếu n là ít hơn m, bạn sẽ có thể đưa ra một giá trị của LTE n m. Nếu không, bạn không thể. Đây là những gì các Curry-Howard isomorphism là tất cả về.

Bây giờ chúng ta đã sẵn sàng để xác định AShorterVec: để xây dựng một giá trị của AShorterVec a n bạn cần để có thể chứng minh rằng nó ngắn hơn n bằng cách cung cấp một giá trị của LTE m n. Khi bạn so khớp mẫu trên hàm tạo AShorterVec, nó sẽ cung cấp cho bạn bằng chứng để bạn có thể tính toán với nó.

data AShorterVec a n = forall m. AShorterVec (LTE m n) (Vec a m) 

biên dịch chỉ với một thay đổi nhỏ: chúng tôi phải thao tác đối tượng bằng chứng này.

takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n 
takeWhile f Nil = AShorterVec ZLte Nil 
takeWhile f (x :- xs) = case takeWhile f xs of 
          AShorterVec prf ys -> if f x 
                then AShorterVec (SLte prf) (x :- ys) 
                else AShorterVec ZLte Nil 

---

Một cách khác để cung cấp cho một loại để takeWhile là để đẩy trên ràng buộc về thời gian vào kiểu trả về chính nó, chứ không phải mang nó xung quanh như dữ liệu. Cách tiếp cận này phân phối với bất kỳ wranglings với Natty, điều khoản bằng chứng như LTE, và định lượng tồn tại.

data ShorterVec a n where 
    SNil :: ShorterVec a n 
    SCons :: a -> ShorterVec a n -> ShorterVec a (S n) 

Một lần nữa, ShorterVec a n biểu thị tập hợp các vectơ không quá n. Cấu trúc của ShorterVec là gợi nhớ của finite sets, nhưng được dịch từ thế giới của naturals vào thế giới của vectơ. Một vector trống ngắn hơn bất kỳ độ dài nào bạn quan tâm đến tên; một ô khuyết điểm tăng giới hạn trên nhỏ nhất hợp lệ bởi một. Lưu ý rằng giá trị của n không bao giờ được xác định đầy đủ bởi một giá trị loại ShorterVec, vì vậy bạn có thể cung cấp bất kỳ giới hạn trên hợp lệ nào cho một số ShorterVec. Hai biểu thức đều nổi-gõ:

ok1 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S (S Z))) 
ok2 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S Z)) 

nhưng điều này không phải là:

-- notOk = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S Z) -- the vector is longer than our stated upper bound. 

Sử dụng kiểu dữ liệu này, bạn có thể viết một phiên bản đẹp đơn giản của takeWhile mà trông giống hệt như phiên bản danh sách ban đầu :

takeWhile :: (a -> Bool) -> Vec a n -> ShorterVec a n 
takeWhile f Nil = SNil 
takeWhile f (x :- xs) = if f x 
         then SCons x (takeWhile f xs) 
         else SNil 

Giải thích các giả định của chúng tôi về loại đã làm cho chức năng đơn giản hơn, nhưng bạn phải trả chi phí cho loại khác d để chuyển đổi sang và từ. Bạn có thể dịch từ ShorterVec trở lại phiên bản đã sử dụng cặp phụ thuộc bằng cách đo chiều dài.

toAVec :: ShorterVec a n -> AVec a 
toAVec SNil = AVec Zy Nil 
toAVec (SCons x xs) = case toAVec xs of 
          AVec n ys -> AVec (Sy n) (x :- ys) 

---

Chúng tôi bắt đầu bằng cách sử dụng độc thân để buộc chủng loại và giá trị với nhau, và các loại hiện sinh để quấn lên thông tin thời gian chạy về dữ liệu với dữ liệu riêng của mình.Sau đó, theo ý tưởng của @ chi, chúng tôi đã mã hóa (một phần) độ chính xác của takeWhile vào chữ ký loại bằng cách sử dụng thuật ngữ chứng minh. Sau đó, chúng tôi đã đưa ra một cách để nướng bất biến chiều dài vào loại trả về trực tiếp, phân phát với sự cần thiết phải chứng minh bất kỳ định lý.

Một khi bạn đã có được hương vị của chương trình được đánh máy phụ thuộc vào lưỡi của bạn, thật khó để quay trở lại cách cũ. Các hệ thống kiểu biểu thức cung cấp cho bạn ít nhất ba ưu điểm: bạn có thể viết các chương trình hợp lệ mà các ngôn ngữ khác sẽ không cho phép (hoặc buộc bạn phải sao chép mã); bạn có thể viết nhiều loại có ý nghĩa hơn cho cùng chức năng, hứa hẹn mạnh hơn; và bạn có thể chứng minh tính chính xác của các chương trình của mình theo cách có thể kiểm tra bằng máy.

Haskell chưa được thiết lập cho nó. Một vấn đề là các singleton tạo các kiểu ràng buộc và các giá trị không cần thiết phức tạp: sự khác biệt Nat - Natty gây ra sự bùng nổ của mã soạn sẵn, hầu hết trong số đó tôi đã tha cho bạn, để trộn lẫn giữa các kiểu và giá trị. (Phần lớn bản mẫu này có thể được tự động hóa - đó là những gì the singletons library cung cấp cho bạn.) Nếu chúng tôi muốn chỉ định một khía cạnh khác của tính chính xác của takeWhile - thực tế là tất cả các phần tử của danh sách đầu ra đều thỏa mãn vị từ - chúng ta phải làm việc độc quyền danh sách các hàm đơn vị và các hàm vị từ cấp. Tôi cũng cảm thấy buồn tẻ khi khai báo một loại cấp cao mới mỗi lần tôi muốn định lượng một cái gì đó tồn tại (bạn có thể viết thư viện để trợ giúp điều này, mặc dù chúng thường dẫn đến bản mẫu khác) - chúng ta thiếu các lambdas kiểu cảm ơn vì điều đó. Khó khăn chính khác là những hạn chế trong những gì có thể được thăng cấp loại bằng cách sử dụng DataKinds: GADT và loại tồn tại không thể được quảng bá, vì vậy ví dụ: bạn không thể có mảng đa chiều có hình dạng được biểu thị tĩnh dưới dạng Vec Nat n . Không có hệ thống gõ thực sự phụ thuộc nào làm cho các kiểu phụ thuộc này khó sử dụng!