Limiti della digitazione dipendente in Idris

Question

Ho scritto Haskell per un po 'di tempo ma volevo provare alcuni esperimenti con il linguaggio Idris e la digitazione dipendente. Ho giocato un po 'e ho letto il documento base, tuttavia voglio esprimere un certo stile di funzione e non so come/se è possibile.

Ecco un paio di esempi di quello che desidero sapere se o non può essere espresso:

prima: una funzione che prende due numeri naturali, ma solo il tipo controlla se il primo è più piccolo dell'altro. Quindi f : Nat -> Nat -> whatever dove nat1 è minore di nat2. L'idea è che se un chiamato come f 5 10 funzionerebbe, ma se lo chiamassi come f 10 5 non riuscirebbe a digitare check.

secondo: una funzione che accetta una stringa e un elenco di stringhe che digita solo i controlli se la prima stringa è presente nell'elenco di stringhe.

Sono possibili funzioni come questa in Idris? Se sì, come implementeresti uno dei semplici esempi? Grazie!

EDIT:

Con l'aiuto di diversi utenti le seguenti funzioni di soluzione sono stati scritti:

module Main 

import Data.So 

f : (n : Nat) -> (m : Nat) -> {auto isLT : So (n < m)} -> Int 
f _ _ = 50 

g : (x : String) -> (xs : List String) -> {auto inIt : So (elem x xs)} -> Int 
g x xs = 52 

main : IO() 
main = putStrLn $ show $ g "hai" ["test", "yo", "ban", "hai", "dog"] 

Queste soluzioni attuali non funzionano per i grandi casi. Ad esempio, se si esegue f con numeri superiori a qualche migliaio, l'operazione richiede sempre (non letteralmente). Penso che questo sia dovuto al fatto che il controllo del tipo è attualmente basato sulla ricerca. Un utente ha commentato che è possibile fornire un suggerimento a scrivendo personalmente la prova. Supponendo che questo è ciò che è necessario come si potrebbe scrivere una prova per uno di questi casi semplici?

Answer 1

I'm not especially fond of So, o addirittura di avere termini di prova evitabili che si aggirano nei programmi. È più soddisfacente tessere le tue aspettative nel tessuto dei dati stessi. Scriverò un tipo per "numeri naturali più piccoli di n".

data Fin : Nat -> Set where 
    FZ : Fin (S n) 
    FS : Fin n -> Fin (S n) 

Fin è un tipo di dati numerico come - confrontare la forma di FS (FS FZ) con quella del numero naturale S (S Z) - ma con ulteriori strutture tipo-livello. Perché si chiama Fin? Esistono precisamente n membri univoci del tipo Fin n; Fin è quindi la famiglia di set finiti.

Voglio dire: Fin è davvero una sorta di numero.

natToFin : (n : Nat) -> Fin (S n) 
natToFin Z = FZ 
natToFin (S k) = FS (natToFin k) 

finToNat : Fin n -> Nat 
finToNat FZ = Z 
finToNat (FS i) = S (finToNat i) 

Ecco il punto: un valore Fin n deve essere più piccolo rispetto al suo n.

two : Fin 3 
two = FS (FS FZ) 
two' : Fin 4 
two' = FS (FS FZ) 
badTwo : Fin 2 
badTwo = FS (FS FZ) -- Type mismatch between Fin (S n) (Type of FZ) and Fin 0 (Expected type) 

Mentre ci siamo, non ci sono numeri minori di zero. Vale a dire, Fin Z, un set con cardinalità pari a 0, è un set vuoto.

Uninhabited (Fin Z) where 
    uninhabited FZ impossible 
    uninhabited (FS _) impossible 

Se si dispone di un numero che è meno di n, allora è certamente meno di S n.Abbiamo così un modo per allentare il limite superiore su un Fin:

weaken : Fin n -> Fin (S n) 
weaken FZ = FZ 
weaken (FS x) = FS (weaken x) 

Possiamo anche andare nella direzione opposta, utilizzando il tipo di controllo per trovare automaticamente il più stretto possibile, legato su un dato Fin.

strengthen : (i : Fin n) -> Fin (S (finToNat i)) 
strengthen FZ = FZ 
strengthen (FS x) = FS (strengthen x) 

si può definire tranquillamente la sottrazione di numeri da FinNat numeri che sono più grandi. Possiamo anche esprimere il fatto che il risultato non sarà più grande dell'input.

(-) : (n : Nat) -> Fin (S n) -> Fin (S n) 
n - FZ = natToFin n 
(S n) - (FS m) = weaken (n - m) 

---

che tutte le opere, ma c'è un problema: weaken opere ricostruendo il suo argomento a O (n), e stiamo applicarlo ad ogni chiamata ricorsiva di -, ottenendo un O (n^2) algoritmo per la sottrazione. Che imbarazzo! weaken è davvero lì solo per aiutare il controllo dei caratteri, ma ha un drastico effetto sulla complessità asintotica del tempo del codice. Possiamo andare via senza indebolire il risultato della chiamata ricorsiva?

Bene, abbiamo dovuto chiamare weaken perché ogni volta che incontriamo un S, la differenza tra il risultato e il limite aumenta. Invece di tirare con forza il valore fino al tipo corretto, possiamo chiudere lo spazio tirandolo delicatamente verso il basso per incontrarlo.

(-) : (n : Nat) -> (i : Fin (S n)) -> Fin (S (n `sub` finToNat i)) 
n - FZ = natToFin n 
(S n) - (FS i) = n - i 

Questo tipo si ispira il nostro successo nello stringere un Fin 's legate con strengthen. Il limite sul risultato di - è esattamente il limite necessario.

sub, che ho utilizzato nel tipo, è la sottrazione di numeri naturali. Il fatto che tronca a zero non ci deve preoccupare, perché il tipo di - assicura che non accadrà mai realmente. (Questa funzione può essere trovato nel Prelude sotto il nome di minus.)

sub : Nat -> Nat -> Nat 
sub n Z = n 
sub Z m = Z 
sub (S n) (S m) = sub n m 

La lezione da imparare qui è questo. In un primo momento, la costruzione di alcune proprietà di correttezza nei nostri dati ha causato un rallentamento asintotico. Avremmo potuto rinunciare a fare promesse sul valore di ritorno e tornare a una versione non tipizzata, ma in effetti giving the type checker more information ci ha permesso di arrivare dove stavamo andando senza fare sacrifici.