유형 시스템을 사용하여 출력 길이 대 입력리스트를 점검하십시오.

Question

길이가 인 n 인리스트 L이리스트 J에 인터리브되고 길이가 n + 1 인 것으로 가정하십시오. J의 각 요소에 대해 L의 이웃 중 어느 것이 더 큰지 알고 싶습니다. 다음의 기능은 길이가, 그 입력으로 L 걸리고,리스트 K를 생성 N + 1은 K의 I에게 번째 요소 J.의 I th 요소의 원하는 이웃 같은 것을

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

expand row = reverse (aux row 0 []) 

나는 (I 원래 OCaml로 쓴)이 함수의 결과의 길이는 입력의 길이에 1을 더한 것으로, 비공식적으로, 자신에게 증명할 수 있습니다. 하지만 나는 이 불변하는 타입 시스템을 통해 증명할 수 있다는 것에 관심이 있었기 때문에 하스켈 (나를위한 새로운 언어)에 건너 뛴 입니다.

* 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

첫째, 일부 수입 및 언어 확장 : 우리는 지금 우리가 (자신의 종류) 유형 수준 어떤 데이터를 홍보 할 수 DataKinds (or TypeInType)이

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

import Data.Type.Equality 

때문에 식 레벨 원주민 정말 자격 일반 data (도대체, 이것은 정확히입니다. 동기 부여 예제는 GHC 문서에 대한 이전 링크가 제공합니다!). 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 

---

이 귀하의 질문에 답을 알려줘 - 이런 종류의 물건을 시작하는 것은 새 물건을 많이 포함한다.