Пределы зависимой типизации в Idris

Question

Я писал Haskell какое-то время, но хотел попробовать некоторые эксперименты с языком Idris и зависимой типизацией. Я немного поиграл и прочитал базовый документ, однако я хочу выразить определенный стиль функции и не знаю, как это сделать, если это возможно.

Вот несколько примеров того, что я хотел бы знать, может ли быть выражено:

первая: функция, которая принимает два натуральных числа, но только тип проверки, если первый меньше, чем другие. Итак, f : Nat -> Nat -> whatever где nat1 меньше nat2. Идея заключается в том, что если вызванный так называемый f 5 10 будет работать, но если бы я назвал его как f 10 5, он не смог бы ввести проверку.

second: функция, которая берет строку и список строк, которые только вводят проверку, если первая строка находится в списке строк.

Возможны ли подобные функции в Идрисе? Если да, то как бы вы реализовали один из простых примеров? Благодаря!

EDIT:

С помощью нескольких пользователей следующие функции решения были написаны:

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

Эти современные решения не работают для больших дел. Например, если вы запустите f с цифрами выше нескольких тысяч, это займет навсегда (не буквально). Я думаю, это потому, что проверка типов в настоящее время основана на поиске. Один пользователь прокомментировал, что можно дать подсказку автору, написав подтверждение самостоятельно. Предполагая, что это необходимо, как написать такое доказательство для любого из этих простых случаев?

Answer 1

I'm not especially fond of So, или, действительно, во избежание использования исключаемых терминов, работающих в программах. Это более удовлетворительно, чтобы сплести ваши ожидания в ткань самих данных. Я собираюсь записать тип для «натуральных чисел, меньших n».

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

Fin представляет собой число типа типа данных - сравните форму FS (FS FZ) с тем, что из натурального числа S (S Z) - но с некоторой дополнительной структурой типа уровня. Почему это называется Fin? Есть точно n уникальных членов типа Fin n; Fin является, таким образом, семейством конечных множеств.

Я имею в виду: 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) 

Вот точка: значение Fin n должно быть меньше, чем его 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) 

Пока мы находимся в нем, нет никаких чисел, меньших нуля. То есть Fin Z, набор с мощностью 0, является пустым множеством.

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

Если у вас есть число, которое меньше, чем n, то это, конечно, меньше, чем S n.Таким образом, у нас есть способ разрыхления верхней границы на Fin:

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

Мы также можем пойти другим путем, с помощью проверки типов автоматически найти сжатые возможно ограничение на данном Fin.

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

можно смело определить вычитание Fin чисел от Nat чисел, которые больше. Мы также можем выразить тот факт, что результат не будет больше, чем вход.

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

---

То, что все работает, но есть одна проблема: weaken работы по восстановлению своего аргумента в O (N) времени, и мы применяем его при каждом рекурсивном вызове -, уступая O (п^2) алгоритм вычитания. Как неловко! weaken действительно существует, чтобы помочь проверять тип, но он оказывает радикальное влияние на асимптотическую сложность кода. Можем ли мы уйти, не ослабив результат рекурсивного вызова?

Ну, нам нужно было позвонить weaken, потому что каждый раз, когда мы сталкиваемся с S, разница между результатом и границей возрастает. Вместо того, чтобы энергично вытягивать значение до правильного типа, мы можем закрыть зазор, осторожно потянув его вниз, чтобы встретить его.

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

Этот тип вдохновлен нашего успеха в затягивании Fin «S связанные с strengthen. Оценка по результату - точно такая же, как и должно быть.

sub, который я использовал в типе, является вычитанием натуральных чисел. Тот факт, что он обрезается нулем, не беспокоит нас, потому что тип - гарантирует, что он никогда не произойдет. (Эта функция может быть найдена в Prelude под названием minus.)

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

Урок, который следует извлечь здесь это. Сначала построение некоторых свойств корректности в наших данных вызвало асимптотическое замедление. Мы могли отказаться от обещаний о возврате и вернуться к нетипизированной версии, но фактически giving the type checker more information позволил нам добраться туда, куда мы направлялись, не жертвуя.