आउटपुट बनाम इनपुट सूची की लंबाई की जांच करने के लिए टाइप सिस्टम का उपयोग

Question

मान लीजिए कि लंबाई एन के साथ सूची एल, लंबाई एन + 1 के साथ सूची जे में इंटरलीव किया गया है। हम जानना चाहते हैं, जे के प्रत्येक तत्व के लिए, एल के पड़ोसियों में से कौन सा बड़ा है। निम्नलिखित समारोह भी लंबाई के अपने इनपुट के रूप में एल लेता है, और एक सूची कश्मीर पैदा करता है, n + 1, इस तरह के मैं कश्मीर वें तत्व जे के मैं वें तत्व के वांछित पड़ोसी है कि

aux [] prev acc = prev:acc 
aux (hd:tl) prev acc = aux tl hd ((max hd prev):acc) 

expand row = reverse (aux row 0 []) 

मैं, अपने आप को साबित कर सकते हैं अनौपचारिक रूप से, यह है कि इस समारोह (जो मैं मूल रूप OCaml में लिखा था) का परिणाम की लंबाई इनपुट की लंबाई एक से अधिक है। लेकिन मैं हास्केल (मेरे लिए एक नई भाषा) तक पहुंच गया क्योंकि मुझे होने में दिलचस्पी है जो इस आविष्कार के प्रकार सिस्टम के माध्यम से साबित करने में सक्षम है।

* Could not deduce: (m1 :+: S (S m)) ~ S (m1 :+: S m) 
    from the context: n ~ S m1 
    bound by a pattern with constructor: 
       Cons :: forall a m. a -> List a m -> List a (S m), 
      in an equation for `aux' 
    at pyramid.hs:23:6-15 
    Expected type: List a (n :+: S m) 
    Actual type: List a (m1 :+: S (S m)) 
* In the expression: aux tl hd (Cons (max hd prev) acc) 
    In an equation for `aux': 
     aux (Cons hd tl) prev acc = aux tl hd (Cons (max hd prev) acc) 
* Relevant bindings include 
    acc :: List a m (bound at pyramid.hs:23:23) 
    tl :: List a m1 (bound at pyramid.hs:23:14) 
    aux :: List a n -> a -> List a m -> List a (n :+: S m) 
     (bound at pyramid.hs:22:1) 

ऐसा लगता है कि मैं क्या करने की जरूरत है:

{-# LANGUAGE GADTs, TypeOperators, TypeFamilies #-} 

data Z 
data S n 

type family (:+:) a b :: * 
type instance (:+:) Z n = n 
type instance (:+:) (S m) n = S (m :+: n) 

-- A List of length 'n' holding values of type 'a' 
data List a n where 
    Nil :: List a Z 
    Cons :: a -> List a m -> List a (S m) 

aux :: List a n -> a -> List a m -> List a (n :+: (S m)) 
aux Nil prev acc = Cons prev acc 
aux (Cons hd tl) prev acc = aux tl hd (Cons (max hd prev) acc) 

हालांकि, अंतिम पंक्ति निम्न त्रुटि पैदा करता है: this previous answer की मदद के साथ, मैं निम्नलिखित के रूप में जहाँ तक प्राप्त करने में सक्षम था क्या संकलक सिखाता है कि (x :+: (S y)) ~ S (x :+: y)। क्या यह संभव है?

वैकल्पिक रूप से, इस प्रणाली के प्रकार के प्रकार के मुकाबले बेहतर उपकरण हैं?

Answer 1

सबसे पहले, कुछ आयात और भाषा एक्सटेंशन:

{-# LANGUAGE GADTs, TypeInType, RankNTypes, TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes #-} 

import Data.Type.Equality 

अब हम DataKinds (or TypeInType) जो हमें (अपनी ही तरह के साथ) प्रकार स्तर तक किसी भी डेटा को बढ़ावा देने के लिए अनुमति देता है, तो प्रकार स्तर प्राकृतिक की वास्तव में लायक नियमित data के रूप में परिभाषित किया जाना चाहिए (हेक, यह बिल्कुल जीएचसी दस्तावेज़ों के पिछले लिंक के प्रेरक उदाहरणों को प्रेरित करता है!)। आपके List प्रकार के साथ कुछ भी नहीं बदलता है, लेकिन (:+:) वास्तव में बंद होना चाहिए प्रकार परिवार (अब Nat की तरह चीजों पर)।

-- A natural number type (that can be promoted to the type level) 
data Nat = Z | S Nat 

-- A List of length 'n' holding values of type 'a' 
data List a n where 
    Nil :: List a Z 
    Cons :: a -> List a m -> List a (S m) 

type family (+) (a :: Nat) (b :: Nat) :: Nat where 
    Z + n = n 
    S m + n = S (m + n) 

अब, क्रम सबूत aux के लिए काम करने के लिए, यह उपयोगी प्राकृतिक संख्या के लिए singleton types परिभाषित करने के लिए है।

-- A singleton type for `Nat` 
data SNat n where 
    SZero :: SNat Z 
    SSucc :: SNat n -> SNat (S n) 

-- Utility for taking the predecessor of an `SNat` 
sub1 :: SNat (S n) -> SNat n 
sub1 (SSucc x) = x 

-- Find the size of a list 
size :: List a n -> SNat n 
size Nil = SZero 
size (Cons _ xs) = SSucc (size xs) 

अब, हम कुछ सामान साबित करने के लिए आकार में हैं। Data.Type.Equality से, a :~: b एक प्रमाण प्रस्तुत करता है कि a ~ b। हमें अंकगणित के बारे में एक साधारण बात साबित करने की आवश्यकता है।

-- Proof that  n + (S m) == S (n + m) 
plusSucc :: SNat n -> SNat m -> (n + S m) :~: S (n + m) 
plusSucc SZero _ = Refl 
plusSucc (SSucc n) m = gcastWith (plusSucc n m) Refl 

अंत में, हम aux में इस सबूत का उपयोग करने के gcastWith उपयोग कर सकते हैं। ओह और आप Ord a बाधा खो रहे थे।:)

aux :: Ord a => List a n -> a -> List a m -> List a (n + S m) 
aux Nil prev acc = Cons prev acc 
aux (Cons hd tl) prev acc = gcastWith (plusSucc (size tl) (SSucc (size acc))) 
             aux tl hd (Cons (max hd prev) acc) 

-- append to a list 
(|>) :: List a n -> a -> List a (S n) 
Nil |> y = Cons y Nil 
(Cons x xs) |> y = Cons x (xs |> y) 

-- reverse 'List' 
rev :: List a n -> List a n 
rev Nil = Nil 
rev (Cons x xs) = rev xs |> x 

---

मुझे पता है अगर यह आपके सवाल का जवाब दें - बात की इस तरह के साथ शुरू हो रही नई सामग्री का एक बहुत कुछ शामिल है।