Или я торможу?

лол ульман и ахо выиграли ацм тюринг

Обнаружилось, что на тайплевел хаскеле есть полноценные зависимые типы, в намного большем смысле чем просто "можно писать a -> (x :: a) -> ..."

Продолжаю изучать в поисках ограничений

Примеры:

- натуральные числа и несколько простых доказательств о коммутативности сложения и умножения:
https://gist.github.com/kana-sama/9185b30b45bd9817f11361e424a8abc7

- простое доказательство (x / 2) * 2 = x для всех четный натуральных чисел:
https://gist.github.com/kana-sama/b029dfa1b1665b207259b58588659a1a

- сигма-типы и работа с ними (тот же безопасный Half :: Even -> Nat)
https://gist.github.com/kana-sama/bd3ec6ddc19846665d9d1f632483550a

для сборки нужен ghc 8.10+

Из проблем:
- отсутствие лямбд приводит к тому, что все функции вида f (\x -> y) превращаются в специализированные топлевел функции, который делают то же самое

лол ульман и ахо выиграли ацм тюринг

можно с глупыми вопросами поприставать? я теорию завтипов в голову себе ещё не загрузил до конца, поэтому вот смотрю я на последний пример и вижу фигу. Допустим хочу я быть уверен что в списке есть данный элемент. Что и куда надо приложить, чтобы проняло? В каком-нибудь Idris я мог бы написать что-то такое:

data Elem : a -> List a -> Type where
     Here : Elem x (x :: xs)
     There : (later : Elem x xs) -> Elem x (y :: xs)

data ListWith1T : Type where
     ListWith1 : (xs : List Int) -> { auto ok : Elem 1 xs } -> ListWith1T

test : ListWith1T
test = ListWith1 [0,1,2,3] -- ok

test2 : ListWith1T
test2 = ListWith1 [0,4,2,3] -- error

Понятно что тут ещё auto, на самом деле

test =

ListWith1

[0,1,2,3] (There Here)

но всё же.

через десять лет может дядя боб выиграет

хотя может и вывести как-то получится