Come posso esprimere il tipo di "takeWhile per i vettori"?

Question

Principiante Haskell qui. Ho definito i seguenti tipi:

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

sto cercando di scrivere la funzione, takeWhileVector che si comporta come TakeWhile fa nelle liste, ma su vettori.

mia implementazione è la seguente:

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 

Questo non compila e produce il seguente errore:

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) 

avrei pensato che la mia definizione di tipo per takeWhileVector dice quanto segue:

Per tutti i tipi 'a' e 'n' di tipo Nat, questa funzione restituisce 'Vector a m', dove 'm' è gentile Nat.

Devo modificare la firma del tipo di takeWhileVector per essere più specifica in modo che mostri che il risultato è Vector a (m :: Nat)? Altrimenti, come posso cambiarlo per farlo compilare?

Answer 1

Il tipo suggerisci non può essere attuato, vale a dire che non è abitata:

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

ricordare che il chiamante sceglie le variabili di tipo a,n,m. Ciò significa che il chiamante può utilizzare la tua funzione come ad es.

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

che è una sciocchezza, dal momento che non si può produrre alcuni a s se hai nessuno all'inizio. Ancora più praticamente, il chiamante di questa funzione non è pensato per essere in grado di scegliere quanti risultati avere e passare una funzione completamente indipendente - che sarebbe in disaccordo con la semantica prevista di takeWhile.

Credo che quello che realmente dire è qualcosa di simile

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

salvo che exists non è la sintassi Haskell valido. Invece, è necessario qualcosa di simile

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

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

Answer 2

Non c'è modo di sapere in modo statico la lunghezza del Vec restituito da takeWhileVec: esso dipende dai valori contenuti nella Vec, e la funzione che si usa. Tuttavia, ciò che posso fare è darti un valore che puoi associare a impara a la lunghezza dello Vec. Immettere singleton values.

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

Per una data n di tipo Nat, v'è esattamente un valore (non undefined) di tipo Natty n. Quindi, se si sa qualcosa su un Natty, si sa anche qualcosa sulla sua associata tipo di livello Nat. *

Perché non possiamo semplicemente usare Nat per questo scopo? Haskell mantiene una separazione tra valori e tipi.Il tipo di livello Nat ha alcuna relazione, diversa da una somiglianza strutturale, al valore di livello Nat: il valore S Z ha un tipo di Nat, non S' Z' - quindi dobbiamo utilizzare Natty, una seconda copia di Nat, per legare manualmente valori e tipi insieme. (Sistemi di reale dipendentemente tipizzato, come Agda consentono di riutilizzare lo stesso Nat sia per il valore-level e calcoli tipo di livello.)

_{* È possibile diffondere la conoscenza anche nel senso opposto, utilizzando le classi di tipo.}

---

Il piano è restituire il vettore di uscita nonché la sua lunghezza come Natty, con i tipi disposti in modo tale che GHC capisce che il Natty rappresenta davvero la sua lunghezza. Si potrebbe prendere in considerazione prima questa variante l'esempio della tua domanda:

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

Ma questo non dice la cosa giusta: stiamo dicendo takeWhile può restituire qualsiasi m di scelta del chiamante, che non è vero! Può solo restituire l'univoco m determinato dalla funzione e dal vettore di input. Come ho detto, questo non è conoscibile in fase di compilazione, quindi dobbiamo mantenere la lunghezza segreta dal compilatore.

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

AVec è un existential type: n appare sul lato destro, ma non a sinistra. Questa tecnica consente di emulare uno dependent pair type: il tipo di Vec dipende dal valore di Natty. Le coppie dipendenti sono utili ogni volta che le proprietà statiche dei dati dipendono da informazioni dinamiche non disponibili in fase di compilazione.

Possiamo scrivere takeWhile semplicemente ora:

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 

abbiamo dovuto buttare via la conoscenza statica della lunghezza del vettore, così come si usa un AVec con una funzione che pone requisiti statici della lunghezza? A causa del modo in cui è stato creato AVec, sappiamo che lo Natty nello slot di sinistra rappresenta la lunghezza del vettore nello slot di destra: entrambi presentano lo stesso parametro di tipo (esistenzialmente nascosto) n. Pertanto, mediante il pattern matching su Natty, viene rilevata la lunghezza dello 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) 

In questo esempio, si cura solo se il vettore è più lungo di uno, così pattern matching on Sy è sufficiente per dimostrare a GHC che dovremmo essere autorizzati a utilizzare head. (Vedere a related answer of mine per un esempio più coinvolto di provare i fatti su AVec s.)

---

@chi menzionati un'idea stuzzicante: si potrebbe desiderare di dimostrare che il vettore restituito da takeWhile non è più lungo del vettore di input.

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

dove AShorterVec è il tipo di vettori non superiore n. La nostra sfida è scrivere la definizione di AShorterVec.

Dati due numeri naturali, come si può essere sicuri che il primo sia inferiore o uguale al secondo? La relazione è induttiva. Se l'operando di sinistra è zero, allora è inferiore o uguale a qualsiasi numero naturale automaticamente. Altrimenti, un numero è inferiore o uguale a un altro se il suo predecessore è inferiore o uguale al predecessore dell'altro. Possiamo codificarlo come una prova costruttiva usando un GADT.

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

Se n è inferiore a m, sarete in grado di venire con un valore di LTE n m. Se non lo è, non puoi. Questo è ciò che è lo Curry-Howard isomorphism.

Ora siamo pronti per definire AShorterVec: per costruire un valore di AShorterVec a n è necessario essere in grado di dimostrare che è più breve di n fornendo un valore di LTE m n. Quando si esegue il pattern-match sul costruttore AShorterVec, si ottiene il proof back per poterlo calcolare.

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

takeWhile compila con solo una piccola modifica: dobbiamo manipolare questo oggetto la prova.

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 

---

Un modo alternativo per dare un tipo di takeWhile è quello di spingere il limite superiore della lunghezza nel tipo ritorno stesso, invece di portare in giro come dati. Questo approccio elimina ogni conflitto con Natty, termini di prova come e quantificazioni esistenziali.

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

Ancora una volta, ShorterVec a n denota l'insieme di vettori non superiore n. La struttura di ShorterVec ricorda lo finite sets, ma tradotta dal mondo dei naturali nel mondo dei vettori. Un vettore vuoto è più corto di qualsiasi lunghezza tu voglia nominare; una cella di controllo aumenta il limite superiore più piccolo valido di uno. Si noti che il valore di n non è mai completamente determinato da un valore di tipo ShorterVec, quindi è possibile assegnare un limite superiore valido a ShorterVec. Queste due espressioni sono entrambi ben tipizzati:

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

ma questo non è:

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

Utilizzando questo tipo di dati, è possibile scrivere una versione splendidamente semplice di takeWhile che appare esattamente come la versione lista originale :

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 

rilassante nostre ipotesi circa il tipo ha fatto la funzione più semplice da implementare, ma si paga il costo di avere un altro tipo che nee d per convertire da e verso. Puoi tradurre da ShorterVec indietro nella versione che utilizzava una coppia dipendente misurando la lunghezza.

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) 

---

Abbiamo iniziato utilizzando singletons per legare i tipi e valori insieme, e tipi esistenziali per concludere informazioni di runtime sui dati con i dati stessi.Quindi, seguendo l'idea di @ chi, abbiamo codificato (una parte della) correttezza di takeWhile nella firma del tipo usando un termine di prova. Poi abbiamo trovato un modo per infornare la lunghezza invariabile nel tipo di ritorno direttamente, senza la necessità di dimostrare alcun teorema.

Una volta ottenuto il gusto della programmazione tipograficamente basata sulla lingua, è difficile tornare alla vecchia maniera. I sistemi di tipo espressivo offrono almeno tre vantaggi: puoi scrivere programmi validi che altre lingue potrebbero non consentire (o costringerti a duplicare il codice); puoi scrivere tipi più significativi per le stesse funzioni, facendo promesse più forti; e puoi dimostrare la correttezza dei tuoi programmi in modo controllabile dalla macchina.

Haskell non è impostato per questo, però. Un problema è rappresentato dal fatto che i singleton rendono inutilmente complessi i tipi e i valori vincolanti: la distinzione Nat - Natty provoca un'esplosione di codice boilerplate, la maggior parte di cui vi ho risparmiato, per mescolare i tipi ei valori. (Gran parte di questo boilerplate può essere automatizzato - questo è quello che ti dà the singletons library.) Se volessimo specificare un altro aspetto della correttezza di takeWhile - il fatto che tutti gli elementi dell'elenco di output soddisfino il predicato - dovremmo lavorare esclusivamente con elenchi di singleton e funzioni di predicato a livello di codice. Trovo anche noioso dichiarare un nuovo tipo di livello superiore ogni volta che voglio quantificare qualcosa in modo esistenziale (puoi scrivere librerie per aiutare con questo, anche se spesso si traducono in altre regole) - abbiamo la mancanza di lambda di livello testo per grazie per quello L'altra difficoltà principale sono le restrizioni in ciò che può essere promosso a livello di tipo usando DataKinds: GADT e tipi non esistenziali non possono essere promossi, quindi per esempio non si può avere un array multidimensionale la cui forma è espressa staticamente come Vec Nat n . Nessun vero sistema tipizzato in modo dipendente rende i tipi dipendenti così difficili da usare!