Ograniczenia pisania zależnego w Idrisie

Question

Piszę Haskella już od jakiegoś czasu, ale chciałem spróbować eksperymentów z językiem Idris i uzależnienia od pisania. Zagrałem trochę i przeczytałem podstawowy dokument, ale chcę wyrazić pewien styl funkcji i nie wiem jak/jeśli to możliwe.

Oto kilka przykładów tego, co chcę wiedzieć, czy nie można wyrazić:

pierwszy: funkcja, która zajmuje dwie liczby naturalne, ale tylko wpisać czeki, jeśli pierwszy jest mniejszy niż drugi. Tak więc f : Nat -> Nat -> whatever gdzie nat1 jest mniejsze niż nat2. Chodzi o to, że gdyby zadzwonił jak f 5 10, to by zadziałało, ale jeśli nazwałbym to jak f 10 5, nie dałoby się sprawdzić.

sekunda: funkcja, która pobiera ciąg znaków i listę napisów, które są wpisywane, sprawdza tylko, czy pierwszy ciąg znaków znajduje się na liście ciągów znaków.

Czy takie funkcje są możliwe w Idris? Jeśli tak, to jak zaimplementować jeden z prostych przykładów? Dzięki!

EDIT:

Z pomocą kilku użytkowników następujące funkcje rozwiązanie zostało napisane:

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

te obecne rozwiązania nie działają dla dużych sprawach. Na przykład, jeśli uruchamiasz f z liczbami powyżej kilku tysięcy, trwa to zawsze (nie dosłownie). Myślę, że dzieje się tak dlatego, że sprawdzanie typu jest obecnie oparte na wyszukiwaniu. Jeden z użytkowników skomentował, że możliwe jest podanie podpowiedzi na auto poprzez samodzielne napisanie dowodu. Zakładając, że jest to potrzebne, jak można by napisać taki dowód na jeden z tych prostych przypadków?

Answer 1

I'm not especially fond of So, lub w istocie o możliwych do uniknięcia dowodach w ogóle w programach. Bardziej satysfakcjonujące jest splatanie twoich oczekiwań w tkankę danych. Zamierzam zapisać typ dla "liczb naturalnych mniejszych niż n".

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

Fin jest to typ danych jak numer - porównaj kształt FS (FS FZ) z tym naturalnej liczby S (S Z) - ale z dodatkowymi struktury typu szczebla. Dlaczego nazywa się Fin? Jest dokładnie n unikalnych członków typu Fin n; Fin jest zatem rodziną skończonych zestawów. Jest to numer: Fin.

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) 

Oto punkt: wartość Fin n musi być mniejszy niż jego 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) 

Podczas gdy jesteśmy przy tym, nie ma żadnych liczb mniej niż zero. Innymi słowy, Fin Z, zbiór o liczności 0 jest zbiorem pustym.

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

Jeśli masz numer, który znajduje się mniej niż n, to jest to z pewnością mniej niż S n.Mamy więc sposób odkręcając górną granicę na Fin:

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

Możemy też pójść w drugą stronę, za pomocą sprawdzania typu automatycznie znaleźć ścisły możliwe granicę na danym Fin.

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

Można bezpiecznie określić odejmowanie Fin numerach od Nat liczb, które są większe. Możemy również wyrazić fakt, że wynik nie będzie większy niż dane wejściowe.

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

---

że wszystkie prace, ale jest pewien problem: weaken dzieła odbudowy jej argument w O (n) czasu, a my jej stosowania na każdym rekurencyjnym wywołaniem -, uzyskując O (n^2) algorytm do odejmowania. Ale wstyd! weaken jest tylko tam, aby pomóc w sprawdzaniu typów, ale ma drastyczny wpływ na asymptotyczną złożoność kodu w czasie. Czy możemy uciec bez osłabienia wyniku rekursywnego połączenia?

Cóż, musieliśmy zadzwonić pod numer weaken, ponieważ za każdym razem, gdy napotykamy numer S, różnica między wynikiem a granicą rośnie. Zamiast forsownego przyciągania wartości do właściwego typu, możemy zamknąć lukę, delikatnie pociągając za typ, aby go spełnić.

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

Ten typ jest inspirowane przez naszego sukcesu w zaciśnięcie Fin „s związane z strengthen. Ograniczenie wyniku - jest dokładnie tak ścisłe, jak powinno być.

sub, którego użyłem w typie, to odejmowanie liczb naturalnych. Fakt, że obcina on zero, nie musi nas niepokoić, ponieważ typ - zapewnia, że ​​nigdy się nie wydarzy. (Ta funkcja może być znaleziony w Prelude pod nazwą minus.)

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

Lekcja na przyszłość tutaj jest to. Na początku, dodanie pewnych właściwości poprawności do naszych danych spowodowało asymptotyczne spowolnienie. Moglibyśmy zrezygnować z obietnic dotyczących wartości zwrotu i wrócić do wersji bez typu, ale w rzeczywistości giving the type checker more information pozwolił nam dotrzeć tam, dokąd zmierzamy, bez poświęceń.