Jak mogę wyrazić typ "takeWhile for vector"?

Question

początkujący Haskell tutaj. Mam zdefiniowane następujące typy:

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

Próbuję napisać funkcję, takeWhileVector która zachowuje taki sam jak takeWhile robi na listach, ale na wektorach.

Moje wdrożenia jest w następujący sposób:

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 

nie opracowuje i produkuje następujący błąd:

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) 

myślałem, że moja definicja typu dla takeWhileVector mówi co następuje:

Dla wszystkich typów "a" i "n" rodzaju Nat, funkcja ta zwraca "Wektor a m", gdzie "m" jest rodzaju Nat.

Czy muszę zmienić sygnaturę typową metody TakeWhileVector, aby była bardziej szczegółowa, tak aby wskazywała, że ​​wynikiem jest Vector a (m :: Nat)? W przeciwnym razie, jak mogę to zmienić, aby go skompilować?

Answer 1

Typ proponujesz nie mogą być realizowane, to znaczy, że nie jest zamieszkany:

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

Pamiętaj, że dzwoniący wybierze zmienne typu a,n,m. Oznacza to, że dzwoniący może użyć Twojej funkcji jako np.

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

co jest nonsensem, ponieważ nie może produkować kilka a S Jeżeli masz nic na początku. Nawet bardziej praktycznie, wywołujący tej funkcji nie jest w stanie wybrać, ile wyników ma mieć i przekazać całkowicie niepowiązaną funkcję - to nie zgadzałoby się z zamierzoną semantyką takeWhile.

Chyba co naprawdę myśli to coś

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

wyjątkiem tego, że nie jest ważne exists składni Haskell. Zamiast tego trzeba coś podobnego

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

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

Answer 2

Nie ma mowy, aby statycznie znać długość Vec, który jest zwracany przez takeWhileVec: To zależy od wartości zawartych w Vec i funkcji użyć. Jednakże, co mogę zrobić, to podać wartość, którą można dopasować do wzoru na nauczyć się długości Vec. Wpisz singleton values.

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

Dla danego n od rodzaju Nat istnieje dokładnie jedna (nie undefined) Wartość typu Natty n. Więc jeśli wiesz coś o Natty, można również dowiedzieć się czegoś o jego powiązanego typu poziomie Nat. *

Dlaczego nie możemy po prostu użyć Nat na ten cel? Haskell utrzymuje separację między wartościami i typami.Typ poziomu Nat nie ma związku, inne niż podobieństwa strukturalnego do wartości poziomu Nat: wartość S Z ma typ Nat, nie S' Z' - więc musimy użyć Natty, drugą kopię Nat, ręcznie powiązać wartości i typy razem. (Systemy rzeczywistym zależnie wpisany takie jak Agda pozwalają używać tego samego Nat zarówno dla wartości poziomu i obliczeń typu szczebla.)

_{* Można propagować wiedzę w drugą stronę też, za pomocą klas typu.}

---

Plan powrotu wektora wyjściowego, jak również jego długości jako Natty z typów rozmieszczonych w taki sposób, że GHC zrozumiałym, że Natty rzeczywiście stanowią jego długość. Może najpierw rozważyć tę odmianę na przykład w swoim pytaniu:

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

Ale to nie znaczy uszne: mówimy takeWhile może powrócić żadnego m wyboru rozmówcy, co nie jest prawdą! Może zwrócić tylko unikalny kod m określony przez funkcję i wektor wejściowy. Jak już wspomniałem, jest to nie do poznania w czasie kompilacji, więc musimy zachować długość w tajemnicy przed kompilatorem.

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

AVec jest existential type: n pojawia się na prawej stronie, ale nie w lewo. Ta technika pozwala na emulację modelu dependent pair type: typ Vec zależy od wartości Natty. Pary zależne są przydatne, gdy statyczne właściwości danych zależą od informacji dynamicznych niedostępnych podczas kompilacji.

Możemy napisać takeWhile wprost teraz:

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 

Musieliśmy wyrzucić statycznej wiedzy o długości Vectora, tak jak można użyć AVec z funkcją, która stawia wymagania statyczne długości? Ze względu na konstrukcję AVec wiemy, że Natty w lewym gnieździe reprezentuje długość wektora w prawym gnieździe: oba mają ten sam (istniejący ukryty) parametr typu n. Tak więc, dopasowując do wzoru na Natty, uczymy się długości 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) 

W tym przykładzie, mamy tylko jedno, czy wektor jest dłuższy niż jeden, więc wzorzec dopasowania na Sy wystarczy udowodnić GHC, że powinniśmy mieć prawo do stosowania head. (Patrz a related answer of mine dla bardziej zaangażowanych przykład udowodnienia faktów o AVec s.)

---

@chi wspomniano kuszący pomysł: może chcesz pokazać, że wektor zwrócony przez takeWhile nie jest dłuższy niż wektora wejściowego.

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

gdzie AShorterVec jest typ wektorów nie dłużej niż n. Naszym wyzwaniem jest zapisanie definicji AShorterVec.

Biorąc pod uwagę dwie liczby naturalne, w jaki sposób można mieć pewność, że pierwszy jest mniejszy lub równy drugiemu? Relacja jest indukcyjna. Jeśli lewy operand wynosi zero, to jest on mniejszy lub równy dowolnej liczbie naturalnej automatycznie. W przeciwnym razie liczba jest mniejsza od lub równa innej, jeśli jej poprzednik jest mniejszy lub równy poprzednikowi drugiej. Możemy to zakodować jako dowód konstruktywny za pomocą GADT.

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

Jeśli n jest mniejsza niż m, będziesz w stanie wymyślić wartości LTE n m. Jeśli nie, nie możesz. O to właśnie chodzi w Curry-Howard isomorphism.

Teraz jesteśmy gotowi do zdefiniowania AShorterVec: w celu skonstruowania wartości AShorterVec a n trzeba być w stanie udowodnić, że jest krótszy niż n dostarczając wartość LTE m n. Gdy dopasowujesz wzorce do konstruktora AShorterVec, daje on dowód z powrotem, dzięki czemu można go obliczyć.

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

takeWhile kompiluje tylko z niewielką zmianą: musimy manipulować dowód ten obiekt.

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 

---

Alternatywny sposób daje typ, takeWhile to, aby przyciskać górną granicą długości do samego typu powrotnego, niż jego przenoszenia danych. W tym podejściu zrezygnowano z jakichkolwiek sprzeczek z Natty, warunków sprawdzających, takich jak LTE, i kwantyfikacji egzystencjalnych.

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

Ponownie ShorterVec a n oznacza zbiór wektorów nie dłużej niż n. Struktura ShorterVec przypomina finite sets, ale została przetłumaczona ze świata naturałów na świat wektorów. Pusty wektor jest krótszy niż jakakolwiek długość, którą chcesz nazwać; komórka cons zwiększa najmniejszą ważną górną granicę o jedną. Zauważ, że wartość n nigdy nie jest w pełni określona przez wartość typu ShorterVec, więc możesz podać dowolną ważną górną granicę do ShorterVec. Te dwa wyrażenia są zarówno dobrze wpisane:

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

ale ten nie jest:

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

Użycie tego typu danych, można napisać pięknie prostą wersję takeWhile który wygląda dokładnie jak na pierwotnej liście wersji :

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 

Reszta nasze założenia o typ dokonał funkcja prostsze do wykonania, ale płacisz koszt posiadania innego rodzaju którym nee d, aby przekonwertować na i z. Możesz przetłumaczyć z wersji ShorterVec na wersję, która używała pary zależnej, mierząc jej długość.

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) 

---

Zaczęliśmy używając pojedynczych związać rodzajów i wartości razem i rodzaje egzystencjalne owinąć się informacja o danych z wykonania samych danych.Następnie, idąc za pomysłem @ chi, zakodowaliśmy (jedną część) z poprawności do podpisu typu za pomocą proof-term. Potem wymyśliliśmy sposób na wypalenie niezmiennika długości bezpośrednio w typie zwracania, rezygnując z potrzeby udowodnienia jakichkolwiek twierdzeń.

Kiedy już poczujesz smak języka programowania zależnie od jego rodzaju, trudno jest wrócić do dawnego sposobu. Ekspresyjne systemy typów dają co najmniej trzy zalety: można pisać poprawne programy, których inne języki by nie akceptowały (lub zmuszać do duplikowania kodu); możesz pisać bardziej znaczące typy dla tych samych funkcji, co czyni silniejsze obietnice; i możesz udowodnić poprawność swoich programów w sposób umożliwiający sprawdzenie maszyny.

Haskell nie jest do tego przystosowany. Jednym problemem jest to, że singletony sprawiają, że typy i wartości wiążące stają się niepotrzebnie skomplikowane: rozróżnienie powoduje eksplozję kodu głównego, którego większość oszczędziłem, aby przetasować między typami i wartościami. (Znaczna część tej karty może być zautomatyzowana - to daje the singletons library.) Jeśli chcielibyśmy określić inny aspekt poprawności takeWhile - fakt, że wszystkie elementy listy wyników spełniają predykat - musielibyśmy pracować wyłącznie z listy singletonów i funkcje predykatów na poziomie typu. Uważam także, że nudne jest deklarowanie nowego typu najwyższego poziomu za każdym razem, gdy chcę coś zilustrować (można pisać biblioteki, aby pomóc w tym, chociaż często skutkują one innym elementem) - mamy brak lambd dziękuję za to. Inną główną trudnością są ograniczenia w tym, co można awansować do poziomu typu przy użyciu DataKinds: GADT i typy egzystencjalne nie mogą być promowane, więc na przykład nie można mieć wielowymiarowej tablicy, której kształt jest wyrażany statycznie jako Vec Nat n . Nie ma prawdziwego, zależnego systemu, który sprawia, że ​​trudne do użycia typy zależne!