Зависимые типы, жидкие типы. Что лучше?

Что значить жидкие?

Что значить жидкие?

https://dl.acm.org/doi/10.1145/1375581.1375602

Мне кажется, несмотря на то что вроде как жидкие типы выглядят проще, эта простота обманчива.

Похоже, внутри жидких типов зависимые типы. Статья, цитата:

We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation.

Соотвественно, вся сложность работы с зависимыми типами сохранится. И как только потребуется что то сложнее хеллоуворда и банальной проверки диапазонов на входе нерекурсивной функции (например, чтобы срабатывала проверка на входе одной функции рекурсивной фуркции и сочеталась с проверкой на выходе другой), то придётся понимать как устроены доказательства.

При этом в языках с зависимыми типами есть инструменты для работы со всей этой машинерией (показываются цели, есть тактики, в идрисе есть рефлексия).

Жидкие типы выглядят меньшим бойлерплейтом и меня вчера посещала идея о гипотетической возможности прикрутить их к идрису и назвать как-то вроде LiquidIdris. Но

1) кажется, что жидкие типы должны быть менее выразительны (иначе за счёт чего достигается простата и возможность использовать Хиндли-Милнера для вывода?)

2) в том же Идрисе не настолько много бойлерплейта, чтобы заморачиваться. В конце концов сложность зависимых типов совсем не в сложности их написания, а в сложности доказательств (как и жидких).

Хотя может быть какие то улучшения стоит привнести в виде сахара.

Бред какой то зачем для этого отдельная терминология. Сумасшедшие.

Вы затронули сложную тему.
Задавать этот вопрос следует, ИМО, в другой рассылке.

А мир пока еле на статику переходит. Через 10-15 лет будет что-то совершенно специфическое. И это хорошо!

Обычного Haskell явно не хватает.

В IO жизни он теряет простоту и красоту выражения.

жидкие типы

Ликвидные.

Вялые есть, жидкие вот появились. Ждем частых типов. И тогда будет полный набор, может быть тогда эти дегенераты уймутся.

https://www.youtube.com/watch?v=XcAAF3mhMOM

Есть еще жирные, скользкие и мутные типы.

«Скользкая типизация» - это звучит, кстати.

Это потому что IO суть вычислительных машин, состояние неизбежно по их дизайну. Функциональщина игрушка дьявола, и пустая трескотня в красивой оболочке.

(например, чтобы срабатывала проверка на входе одной функции рекурсивной фуркции и сочеталась с проверкой на выходе другой), то придётся понимать как устроены доказательства.

{-@ append :: xs:[a] -> ys:[a] -> {v:[a] | (len v) = (len xs) + (len ys)} @-}
append [] ys     = ys
append (x:xs) ys = x : append xs ys

?

Или покажи пример на зависимых типах.

в сложности доказательств (как и жидких)

В случае жидких всё, что нерекурсивно или рекурсивно по одному аргументу доказывается автоматически (как пример с append). То, что не доказывается автоматически, доказывается очень наглядно:

Например, есть рекурсивное определение фибоначчи

{-@ fib::{x:Int | x >=0} -> {r : Int|r>0} @-}
fib :: Int -> Int
fib 0 = 1
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

условие, что результат больше нуля, компилятор выводит автоматически.

и с аккумулятором

{-@ fibacc::Int -> Int -> n:Int -> {n1:Int | n1 >=0 && (n1 >= n || n1 < 2)} -> Int / [n1-n] @-} 
fibacc :: Int -> Int -> Int -> Int -> Int
fibacc _ _ _ 0 = 1
fibacc _ _ _ 1 = 1
fibacc f1 f2 n n1 
 | n == n1 = f1 + f2
 | otherwise = fibacc f2 (f1+f2) (n+1) n1

{-@ fib2::{n:Int | n >=0} -> r:Int @-}
fib2 :: Int -> Int
fib2 n = fibacc 1 1 2 n

В фигурных скобках ограничения жидких типов.

Теперь, если надо доказать, что fib n = fib2 n для всех n можно попробовать просто дописать постусловие:

{-@ fib2::{n:Int | n >=0} -> {r:Int | r = fib n} @-}

Не получается. Компилятор недостаточно умён. Можно написать ему доказательство:

{- fibaccLemma :: f1:Int -> f2:Int -> {k:Int | k >= 0} -> {n:Int | n >=2 && n-k>=2 }  -> { fibacc f1 f2 k n == fibacc f1 f2 k (n-1) + fibacc f1 f2 k (n-2) } / [n-k] @-}
fibaccLemma :: Int -> Int -> Int -> Int -> Proof
fibaccLemma f1 f2 k n | n - k == 2
    = fibacc f1 f2 k n == fibacc f1 f2 k (n-1) + fibacc f1 f2 k (n-2)
    === fibacc f2 (f1+f2) (k+1) n == fibacc f2 (f1+f2) (k+1) (n-1) + f1 + f2
    === fibacc (f1+f2) (f1+f2+f2) (k+2) n == f2+f1+f2+f1+f2
    === f1+f2+f1+f2+f2 == f2+f1+f2+f1+f2
    *** QED
fibaccLemma f1 f2 k n | n - k > 2
    = fibacc f1 f2 k n == fibacc f1 f2 k (n-1) + fibacc f1 f2 k (n-2)
    === fibacc f2 (f1+f2) (k+1) n == fibacc f2 (f1+f2) (k+1) (n-1) + fibacc f2 (f1+f2) (k+1) (n-2)
    ? fibaccLemma f2 (f1+f2) (k+1) n
    *** QED

{-@ fibTheorem :: {n:Int | n >= 0} -> { fib n == fib2 n } @-}
fibTheorem :: Int -> Proof 
fibTheorem 0 = fib 0 == fib2 0
    === 1 == fibacc 1 1 2 0
    === 1 == 1
    *** QED
fibTheorem 1 = fib 1 == fib2 1 
    === 1 == fibacc 1 1 2 1
    === 1 == 1 
    *** QED
fibTheorem n = fib n == fib2 n
    === fib (n-1) + fib (n-2) == fibacc 1 1 2 n
    ? fibaccLemma 1 1 2 n
    === fib (n-1) + fib (n-2) == fibacc 1 1 2 (n-1) + fibacc 1 1 2 (n-2)
    === fib (n-1) + fib (n-2) == fib2 (n-1) + fib2 (n-2)
    *** QED

В случае же зависимых типов доказательство получается почти нечитаемое.

В случае жидких всё, что нерекурсивно или рекурсивно по одному аргументу доказывается автоматически (как пример с append).

Это вряд ли возможно. Или ты бы доказал свой аргмакс. Спецификация которую я написал доказывается индукцией по одному аргументу. Или она не выражается на жидких типах?

{-@ fibacc::Int -> Int -> n:Int -> {n1:Int | n1 >=0 && (n1 >= n || n1 < 2)} -> Int / [n1-n] @-}

что значит Int / [n1-n] ?

Обычного Haskell явно не хватает.

В каком плане не хватает? С refinement types ты в плане выразительности сильно далеко не уедешь. Плюс, это внешняя штука для компилятора, поэтому, например, на кодогенерации не скажется вообще никак.

А зависимых типов в хацкелле просто нет и не факт, что когда-нибудь будут. Можешь синглтонами обмазываться. Мои коллеги вот их очень любят.

В Haskell не хватает возможности писать прикладные приложения. Компиляторы научились писать, хорошо, но этого мало. Как я люблю говорить: качество ЯП определяется не тем, насколько в нем много фич, а тем, насколько их мало, насколько просто и лаконично записывается программа. В принципе, ЯП для кодирования Тьюринг-машин уже постепенно все приходят к одному и тому же формату — из нового можно упомянуть вывод типов или динамическую типизацию с выводом типов JIT, лексические замыкания и прочие формы локализации обработки данных. В остальном это всё сплошные вариации на тему Algol 60 и ML, опционально с ублюдочнейшим сишным синтаксисом, от которого постепенно и неохотно уходят.

прикрутить их к идрису и назвать как-то вроде LiquidIdris

Liquidris.

Бред какой то зачем для этого отдельная терминология. Сумасшедшие

Антоха, ты чо, весь хацкель построен вокруг мозговыносящих определений. Чего только монада стоит. Смотри только не перепутай монаду с функтором. Хаскель изучают только для того, чтобы придумать новое определние чему-нибудь.

Обычного Haskell явно не хватает

Кто сказал?

А зависимых типов в хацкелле просто нет и не факт, что когда-нибудь будут. Можешь синглтонами обмазываться.

Каким образом синглтоны заменяют зависимые типы?

Это вряд ли возможно. Или ты бы доказал свой аргмакс.

В аргмаксе не по одному аргументу. Там произвольная функция и список. И написать некий len1 x от списка я не могу.

что значит Int / [n1-n] ?

«/ [n1-n]» – это указание, что при вычислении конечности алгоритма надо брать критерием разницу n1-n.

В каком плане не хватает? С refinement types ты в плане выразительности сильно далеко не уедешь.

В смысле? Как минимум в этом случае есть нормальные интервальные типы, а не Double для длины предмета (и неважно, что она неотрицательна) и Int для номера бита в байте.

Плюс, это внешняя штука для компилятора, поэтому, например, на кодогенерации не скажется вообще никак.

И что? Потеряется 2% производительности?

А зависимых типов в хацкелле просто нет и не факт, что когда-нибудь будут.

Вот вместо них для всех реальных случаев можно использовать жидкие. AndreyKl всё намекает, что существует пример, который можно написать на зависимых, но нельзя на жидких, но сам пример не приводит.

В Haskell не хватает возможности писать прикладные приложения.

Чем pandoc не прикладное приложение?

В каком плане не хватает?

Как минимум, с жидкими типами для новой специализации монады можно сразу проверить, выполняются ли монадические законы, а не тогда когда всё внезапно поломалось и неясно почему.

Короче хаскел даже по сравнению с Алгол’ом жидко обосрался

В случае же зависимых типов доказательство получается почти нечитаемое.

fib : ℕ -> ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = fib (suc n) + fib n

fibAux : ℕ -> ℕ -> ℕ -> ℕ
fibAux a b 0 = a
fibAux a b (suc n) = fibAux b (a + b) n

fib2 : ℕ -> ℕ
fib2 = fibAux 0 1


fibEqAux : ∀ m n -> fib (m + n) ≡ fibAux (fib m) (fib (suc m)) n
fibEqAux m zero = cong fib (+-identityʳ m)
fibEqAux m (suc n) =
  begin
    fib (m + suc n)
  ≡⟨⟩
    fib (m + (1 + n))
  ≡⟨ sym (cong fib (+-assoc m 1 n)) ⟩
    fib (m + 1 + n)
  ≡⟨ cong fib (cong (_+ n) (+-comm m 1)) ⟩
    fib (suc m + n)
  ≡⟨ fibEqAux (suc m) n ⟩
    fibAux (fib (suc m)) (fib (suc (suc m))) n
  ≡⟨⟩
    fibAux (fib (suc m)) (fib (suc m) + fib m) n
  ≡⟨ cong (λ X -> fibAux (fib (suc m)) X n) (+-comm (fib (suc m)) (fib m)) ⟩
    fibAux (fib (suc m)) (fib m + fib (suc m)) n
  ≡⟨⟩
    fibAux (fib m) (fib (suc m)) (suc n)
  ∎

fibEqBase : ∀ n -> fib n ≡ fibAux 0 1 n
fibEqBase n = fibEqAux 0 n

fibEq : (n : ℕ) -> fib2 n ≡ fib n
fibEq n =
  begin
    fib2 n
  ≡⟨⟩
    fibAux 0 1 n
  ≡⟨ sym (fibEqBase n) ⟩
    fib n
  ∎

По мне так оба доказательства нечитаемы.

это на чём?

Agda. Для тайпчека, если вдруг интересно, понадобится

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

спасибо

Красивое доказательство. Если переписать именно его, будет так:

{-@ LIQUID "--reflection" @-}
import Language.Haskell.Liquid.ProofCombinators 

{-@ type N = {x:Int | x>=0} @-}

{-@ reflect fib @-}
{-@ fib :: N -> N @-}
fib :: Int -> Int
fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)

{-@ reflect fibAux @-}
{-@ fibAux :: N -> N -> n:N -> N / [n] @-}
fibAux :: Int -> Int -> Int -> Int
fibAux a b 0 = a
fibAux a b n = fibAux b (a + b) (n-1)

{-@ reflect fib2 @-}
{-@ fib2 :: N -> N @-}
fib2 :: Int -> Int
fib2 n = fibAux 0 1 n

{-@ fibEqAux :: m:N -> n:N -> { fib (m+n) == fibAux (fib m) (fib (m+1)) n } / [n] @-}
fibEqAux :: Int -> Int -> Proof
fibEqAux m 0 
    = fib (m + 0) == fibAux (fib m) (fib (m+1)) 0
    === fib m == fib m 
    *** QED
fibEqAux m n 
    = fib (m + n)
    === fib ((m+1) + (n-1))
        ? fibEqAux (m+1) (n-1)
    === fibAux (fib (m+1)) (fib ((m+1)+1)) (n-1)
    === fibAux (fib (m+1)) (fib m + fib (m+1)) (n-1)
    === fibAux (fib m) (fib (m+1)) n
    *** QED

{-@ fibEq :: n:N -> { fib2 n == fib n } @-}
fibEq :: Int ->Proof
fibEq n 
    = fib2 n
    === fibAux 0 1 n
    === fibAux (fib 0) (fib 1) n
        ? fibEqAux 0 n
    === fib n
    *** QED

Можно заметить, что по сравнению с Агдой не приходится писать вещи типа

≡⟨ cong (λ X -> fibAux (fib (suc m)) X n) (+-comm (fib (suc m)) (fib m)) ⟩

чтобы обосновать тривиальную коммутативность сложения

А нечитаемость я имел в виду у доказательств наподобие https://github.com/andreykl/argmax/blob/main/argmax.v

Красивое доказательство. Если переписать именно его, будет так:

Спасибо.

Можно заметить, что по сравнению с Агдой не приходится писать вещи типа

Я писал это для себя и максимально вербозно, чтоб разобраться, как вся эта штука работает. Полагаю, что можно написать и компактнее. Но быстрая проверка показала, что полностью самостоятельно она этот кусок вывести не может.

А нечитаемость я имел в виду у доказательств наподобие https://github.com/andreykl/argmax/blob/main/argmax.v

Мда, тактики явно не для людей.

Чем pandoc не прикладное приложение?

Это транслятор. С натяжкой это можно назвать прикладным пердолингом, примерно как sed и imagemagick, но для по-настоящему прикладной роли ему нужен интерактивный интерфейс, в который хаскель не умеет.

А мир пока еле на статику переходит.

Слава богу не весь

Ещё из свежего про liquid haskell - Verifying replicated data types with typeclass refinements in Liquid Haskell. Верифицируют инстансы полугруппы, моноида и FAM для пачки типов.

На самом деле бесмысленность всей этой темы в том, что Haskell без расширений популярен и на нем пишут программы, а всё остальное непопулярно и развивается вяло. Поэтому можно считать, что никаких тенденций нет.

для по-настоящему прикладной роли ему нужен интерактивный интерфейс, в который хаскель не умеет.

Держи: https://github.com/lettier/gifcurry

Достаточно интерактивно?

для по-настоящему прикладной роли ему нужен интерактивный интерфейс, в который хаскель не умеет.

Веба на хацкелле просто дохрена. В том числе и на фронте.

Каким образом синглтоны заменяют зависимые типы?

Заменяют – так себе термин.

Ещё есть https://github.com/lettier/movie-monad

Не надо разубеждать.
Но всё равно, чтобы писать качественно, читаемо, красиво в конце концов, нужен большой опыт с человеком явно умнее тебя, а у таких людей нет времени. Вот и имеем, что имеем по Хаскелу.

Это не лучшее применение Haskell. Если Вас интересует правильное, рекомендую взглянуть на https://github.com/david-janssen/kmonad

И у ребят проблемы с названиями, Вы не находите? Монада головного мозга?

Как минимум в этом случае есть нормальные интервальные типы, а не Double для длины предмета (и неважно, что она неотрицательна) и Int для номера бита в байте.

Это-то да. Это и в базовом языке делается через refined. Алсо, Int blindness – старая проблема. Я вот не очень понимаю, почему для индексации контейнеров используют Int, а не хотя бы Word.

И что? Потеряется 2% производительности?

Нет, я не об этом. Я о том, что нет возможности значения из лапши на LH вывести в обычный хаскелл. То есть, информация идёт только из H в LH, но не обратно.

AndreyKl всё намекает, что существует пример, который можно написать на зависимых, но нельзя на жидких, но сам пример не приводит.

Да, я думаю такой пример тоже должен существовать. Хотя бы потому что refinement types – это налепленные на хацкелловые типы предикаты.

Мне вот здесь объяснение понравилось: https://cs.stackexchange.com/questions/21728/dependent-types-vs-refinement-types

Thus, refinement types are similar to dependent pair types whose second type are restricted to being a decidable predicate.

В принципе, этим определением можно закончить тред :)

Как минимум, с жидкими типами для новой специализации монады можно сразу проверить, выполняются ли монадические законы, а не тогда когда всё внезапно поломалось и неясно почему.

Для любой вообще монады, мне почему-то кажется, может не получиться. Но пруфов сейчас не дам.

Да я всегда всем первым делом говорю, что я на самом деле тупой. Но мне почему-то никто не верит и все пытаются со мной о чём-то спорить.

Для любой вообще монады, мне почему-то кажется, может не получиться.

Или доказал или нет.

Или доказал или нет.

Погоди. А ты точно настоящий ЛОРовец? Потому что здесь так дела не делаются!

Да я всегда всем первым делом говорю, что я на самом деле тупой.

Это я писал о себе.

Это я писал о себе.

Не-не-не, это я писал о тебе. Не путай.

существует пример, который можно написать на зависимых, но нельзя на жидких, но сам пример не приводит.

Короче, вот

In Liquid Haskell, only structural recursive functions on a single argument with a single equation per constructor are allowed to be used in decidable predicates, together with operators from the quantifier-free logic of linear arithmetic and uninterpreted functions (namely ==, <, +, …)

Из этого ограничения можно довольно нехитрым образом вывести пример, который можно сделать на DT, но нельзя на LH.

Правда, это больше похоже на ограничение самого LH, а не refinement types в принципе.

http://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/

Liquid Types are refinement types, that is types that are refined with logical predicates that cannot be arbitrary expressions (like dependent types) but are expressions drawn from a sublanguage.

Liquid Types are a constraint form of refinement types in that logical predicates come from a decidable sublanguage, that is a logical language for which implication checking is decidable. Examples of such decidable languages are quantifier-free theories as arrays, integer linear, set theory etc.

Т.е. можно руками не писать доказательства. Но язык спецификации сильно ограничен.

эскобар.жпг.

нах оно вообще в продакшене нужно?

Держи: https://github.com/lettier/gifcurry
Достаточно интерактивно?

Одно окошко за 4 года разработки? А спасибо нужно сказать мне, потому что значительная доля описания GUI сделана на Glade, который много лет не мог поддерживать невизуальные компоненты из-за багов в самом Glade, которые я пофиксил в процессе реализации поддержки этих невизуальных компонентов. Ну а то, что сама обработка выполняется на ffmpeg/gstreamer/imagemagick — это, я думаю, и так очевидно.