Ít nhất (*)

Question

Có thể thực hiện (*) với ngữ nghĩa ít nghiêm ngặt nhất trong Haskell (tiêu chuẩn Haskell được ưa thích, nhưng phần mở rộng là OK. Sử dụng trình biên dịch internals là gian lận)? Ví dụ, một định nghĩa như vậy nên kết quả trong những điều sau đây là đúng:

0 * ⊥ = 0 
⊥ * 0 = 0 

và chỉ:

⊥ * ⊥ = ⊥ 

tôi có thể xây dựng mô hình phù hợp đáp ứng một trong những trường hợp nêu trên, nhưng không phải cả hai, bởi vì không kiểm tra buộc giá trị.

Answer 1

Có, nhưng chỉ sử dụng tạp chất bị hạn chế.

laziestMult :: Num a => a -> a -> a 
laziestMult a b = (a * b) `unamb` (b * a) 

đây unamb là biến thể "thuần túy" của Conal Elliott là amb. Hoạt động, amb chạy hai phép tính song song, quay trở lại bao giờ đến trước. Denotationally unamb có hai giá trị trong đó một giá trị lớn hơn (theo nghĩa lý thuyết miền) so với giá trị kia và trả về giá trị lớn hơn. Chỉnh sửa: đây cũng là unamb, không phải lub, vì vậy bạn cần phải có chúng bằng nhau trừ khi một là dưới cùng. Vì vậy, bạn có một yêu cầu ngữ nghĩa phải giữ mặc dù nó không thể được thi hành bởi hệ thống kiểu. Điều này được thực hiện một cách cơ bản:

nhiều công việc đi vào hoạt động chính xác với ngoại lệ/quản lý tài nguyên/an toàn luồng.

laziestMult là chính xác nếu * là giao hoán. Đó là "ít nghiêm ngặt" nếu * không nghiêm ngặt trong một đối số.

Để biết thêm, xem câu trả lời Conal's blog của

Answer 2

Phillip JF của chỉ áp dụng cho các lĩnh vực bằng phẳng, nhưng có Num trường mà không phải là bằng phẳng, ví dụ như bẩm lười biếng. Khi bạn đi vào đấu trường này, mọi thứ trở nên khá tinh tế.

data Nat = Zero | Succ Nat 
    deriving (Show) 

instance Num Nat where 
    x + Zero = x 
    x + Succ y = Succ (x + y) 

    x * Zero = Zero 
    x * Succ y = x + x * y 

    fromInteger 0 = Zero 
    fromInteger n = Succ (fromInteger (n-1)) 

    -- we won't need the other definitions 

Điều này đặc biệt quan trọng đối với các bản chất lười biếng hoạt động ít nghiêm ngặt nhất, vì đó là miền sử dụng của chúng; ví dụ. chúng tôi sử dụng chúng để so sánh độ dài của các danh sách có thể vô hạn và nếu hoạt động của nó không kém chặt chẽ, thì điều đó sẽ phân kỳ khi có thông tin hữu ích được tìm thấy.

Đúng như dự đoán, (+) là không giao hoán:

ghci> undefined + Succ undefined 
Succ *** Exception: Prelude.undefined 
ghci> Succ undefined + undefined 
*** Exception: Prelude.undefined 

Vì vậy, chúng tôi sẽ áp dụng các thủ thuật tiêu chuẩn để làm cho nó như vậy:

laxPlus :: Nat -> Nat -> Nat 
laxPlus a b = (a + b) `unamb` (b + a) 

mà dường như để làm việc, lúc đầu

ghci> undefined `laxPlus` Succ undefined 
Succ *** Exception: Prelude.undefined 
ghci> Succ undefined `laxPlus` undefined 
Succ *** Exception: Prelude.undefined 

nhưng trên thực tế nó không

ghci> Succ (Succ undefined) `laxPlus` Succ undefined 
Succ (Succ *** Exception: Prelude.undefined 
ghci> Succ undefined `laxPlus` Succ (Succ undefined) 
Succ *** Exception: Prelude.undefined 

Điều này là do Nat không phải là miền phẳng và unamb chỉ áp dụng cho các tên miền phẳng.Đó là vì lý do này mà tôi xem xét unamb một nguyên thủy cấp thấp không nên được sử dụng ngoại trừ để xác định các khái niệm cấp cao hơn - nó sẽ không liên quan cho dù tên miền là bằng phẳng. Sử dụng unamb sẽ rất nhạy cảm với các trình tái cấu trúc thay đổi cấu trúc miền - cùng một lý do là seq có ngữ nghĩa xấu xí. Chúng ta cần phải khái quát hóa unamb cùng một cách seq được tổng quát thành deeqSeq: điều này được thực hiện trong mô-đun Data.Lub. Đầu tiên chúng ta cần phải viết một ví dụ HasLub cho Nat:

instance HasLub Nat where 
    lub a b = unambs [ 
        case a of 
         Zero -> Zero 
         Succ _ -> Succ (pa `lub` pb), 
        case b of 
         Zero -> Zero 
         Succ _ -> Succ (pa `lub` pb) 
       ] 
     where 
     Succ pa = a 
     Succ pb = b 

Giả sử điều này là đúng, mà không nhất thiết phải là trường hợp (nó tôi thứ ba cố gắng cho đến nay), bây giờ chúng ta có thể viết laxPlus':

laxPlus' :: Nat -> Nat -> Nat 
laxPlus' a b = (a + b) `lub` (b + a) 

và nó thực sự hoạt động:

ghci> Succ undefined `laxPlus'` Succ (Succ undefined) 
Succ (Succ *** Exception: Prelude.undefined 
ghci> Succ (Succ undefined) `laxPlus'` Succ undefined 
Succ (Succ *** Exception: Prelude.undefined 

Vì vậy, chúng tôi được thúc đẩy để khái quát rằng mô hình ít nghiêm ngặt nhất cho toán tử nhị phân giao hoán s là:

leastStrict :: (HasLub a) => (a -> a -> a) -> a -> a -> a 
leastStrict f x y = f x y `lub` f y x 

Ít nhất, nó được đảm bảo là giao hoán. Nhưng, than ôi, có những vấn đề nữa:

ghci> Succ (Succ undefined) `laxPlus'` Succ (Succ undefined) 
Succ (Succ *** Exception: BothBottom 

Chúng tôi hy vọng tổng của hai số đó là ít nhất 2 đến ít nhất là 4, nhưng ở đây chúng tôi nhận được một số mà chỉ ít nhất 2. Tôi không thể đến với một cách để sửa đổi leastStrict để cung cấp cho chúng tôi kết quả chúng tôi muốn, ít nhất là không phải giới thiệu một ràng buộc lớp mới. Để khắc phục vấn đề này, chúng ta cần phải thâm nhập vào các định nghĩa đệ quy, và đồng thời mô hình phù hợp trên cả hai tranh luận tại mỗi bước:

laxPlus'' :: Nat -> Nat -> Nat 
laxPlus'' a b = lubs [ 
    case a of 
     Zero -> b 
     Succ a' -> Succ (a' `laxPlus''` b), 
    case b of 
     Zero -> a 
     Succ b' -> Succ (a `laxPlus''` b') 
    ] 

Và cuối cùng chúng ta có được một cung cấp cho càng nhiều thông tin càng tốt, tôi tin rằng:

ghci> Succ (Succ undefined) `laxPlus''` Succ (Succ undefined) 
Succ (Succ (Succ (Succ *** Exception: BothBottom 

Nếu chúng ta áp dụng cùng một khuôn mẫu để lần, chúng tôi nhận một cái gì đó mà dường như làm việc tốt:

laxMult :: Nat -> Nat -> Nat 
laxMult a b = lubs [ 
    case a of 
     Zero -> Zero 
     Succ a' -> b `laxPlus''` (a' `laxMult` b), 
    case b of 
     Zero -> Zero 
     Succ b' -> a `laxPlus''` (a `laxMult` b') 
    ] 

ghci> Succ (Succ undefined) `laxMult` Succ (Succ (Succ undefined)) 
Succ (Succ (Succ (Succ (Succ (Succ *** Exception: BothBottom 

Không cần phải nói, có một số mã lặp lại ở đây, và phát triển các mô hình để thể hiện các chức năng này một cách ngắn gọn (và do đó với ít cơ hội cho lỗi) nhất có thể sẽ là một bài tập thú vị. Tuy nhiên, chúng tôi có một vấn đề khác ...

asLeast :: Nat -> Nat 
atLeast Zero = undefined 
atLeast (Succ n) = Succ (atLeast n) 

ghci> atLeast 7 `laxMult` atLeast 7 
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ ^CInterrupted. 

Thật đáng sợ. Rõ ràng điều này là bởi vì nó là (ít nhất) theo cấp số mũ trong kích thước của các đối số của nó, giảm dần thành hai nhánh trên mỗi đệ quy. Nó sẽ yêu cầu tinh tế hơn để có được nó để chạy trong thời gian hợp lý.

Lập trình ít nghiêm ngặt là lãnh thổ tương đối chưa được khám phá và cần phải nghiên cứu thêm, cả trong thực hiện và ứng dụng thực tế. Tôi vui mừng bởi nó và coi nó là lãnh thổ hứa hẹn.