Używanie systemu typów do sprawdzania długości wyjścia w zależności od listy wejściowej

Question

Załóżmy, że lista L o długości n jest przeplatana na liście J o długości n + 1. Chcielibyśmy wiedzieć, dla każdego elementu J, który z sąsiadów z L jest większy. następujących funkcji zajmuje L jako wejście i tworzy listy k, również o długości n + 1, tak że I ty element K jest pożądane sąsiadem ı ty element J.

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

expand row = reverse (aux row 0 []) 

mogę udowodnić sobie, nieoficjalnie, że długość wyniku tej funkcji (co ja pierwotnie napisał w SML) jest jednym większa niż długość danych wejściowych. Ale I przeniósł się do Haskell (nowy język dla mnie), ponieważ zainteresowałem się byciem zdolnym do udowodnienia poprzez system typów, który posiada ten niezmiennik. Z pomocą z this previous answer byłem stanie uzyskać w miarę następujące:

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

Jednak ostatnia linia produkuje następujący błąd:

* 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) 

Wydaje się, że to, co trzeba do uczy kompilatora, że ​​(x :+: (S y)) ~ S (x :+: y). czy to możliwe?

Czy istnieją lepsze narzędzia do tego problemu niż system typów?

Answer 1

Po pierwsze, niektóre import i rozszerzenia język:

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

import Data.Type.Equality 

Mamy teraz DataKinds (or TypeInType) co pozwala nam promować żadnych danych na poziomie typu (z własnej naturze), więc Naturals poziomie typu naprawdę zasługują być zdefiniowanym jako zwykły data (heck, to jest dokładnie motywujące przykłady dać poprzednie łącze do dokumentów GHC!). Nic nie zmienia się z twoim typem List, ale (:+:) naprawdę powinien być rodziną typu zamkniętą (teraz nad rzeczami rodzaju 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) 

Teraz, w celu uczynienia dowody pracować aux, warto zdefiniować singleton types dla liczb naturalnych.

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

Teraz jesteśmy w formie, aby zacząć udowadniać pewne rzeczy. Od Data.Type.Equality, a :~: b reprezentuje dowód, że a ~ b. Musimy udowodnić jedną prostą rzecz dotyczącą arytmetyki.

-- 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 

Wreszcie, możemy użyć gcastWith użyć tego dowodu w aux. Och, a ty brakowało ci ograniczenia 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 

---

Daj mi znać, jeśli to odpowiada na twoje pytanie - rozpoczęcie pracy z tego typu rzeczy wiąże się wiele nowych rzeczy.