- PVSM.RU - https://www.pvsm.ru -
Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround [1], написанной на Скале с использованием Shapeless [2]. У библиотеки имеется документация [3], правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил [4] из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT [5]), (полу-) автоматически доказывать теоремы.
Началось все с того, что мне захотелось записать вводный курс по зависимым типам на Скале для конкурса Степика. Не хотелось повторяться, на Идрисе недавно появился хороший курс [6]. Скала была выбрана как один из самых популярных функциональных языков. Погуглил по гитхабу по словам «Скала», «зависимые типы», «HoTT» и наиболее многообещающе выглядела ProvingGround. Сразу дисклеймер — я не утверждаю, что те или иные языки или библиотеки наиболее подходят для программирования с зависимыми типами, автоматического доказательства теорем, работы с HoTT. Можно было взять другие языки или библиотеки — был бы другой курс.
Как известно, Скала — язык с ограниченной поддержкой зависимых типов. Зависимые типы имплементируются в ней (другая [7] точка зрения — эмулируются) с помощью path-dependent типов [8], type-level [9] значений и имплицитов [10]. Объяснять зависимые типы на голой Скале или Скале плюс Shapeless и погрязнуть в технических деталях типа отличия [11] type members от type parameters (дженериков), имплицитов, path-dependent типов, «Aux» паттерна [12], type-level вычислений и т.д. не очень хотелось. Поэтому часть курса была на голой Скале, но бОльшая часть практики — на ProvingGround.
Для задания переменных, термов, типов, функций и т.д. ProvingGround предоставляет свой DSL.
Так можно объявить тип A
и переменную a
этого типа:
val A = "A" :: Type
val a = "a" :: A
т.е. типичное объявление выглядит как
val идентификатор_переменной = "как печатать переменную" :: Тип_переменной
Напечатать терм «красиво» можно с помощью метода .fansi
, вывести его тип — с помощью .typ
:
println(a)
> a : (A : U_0)
println(a.fansi)
> a
println(a.typ)
> A : U_0
println(a.typ.fansi)
> A
Можно задать переменную детальнее:
val a : Term = "a" :: A
Здесь A
— это тип в библиотеке ProvingGround, т.е. HoTT-тип, а Term
— это тип в Скале.
Итак, если мы задаем переменную, то пишем тип после ::
, а если у нас уже есть терм, то проверить его тип можно с помощью !:
a !: A
То, что эта строчка компилируется, означает, что тип указан правильно.
Небольшое напоминание о типах. Есть значения и есть типы. У каждого значения есть его тип. Зависимый тип [13] — это тип, зависящий от значения (другого типа). Например, список двух строк и список трех строк — это значения одного и того же типа — список строк. Но если вынести информацию о числе элементов на уровень типа, то получим зависимый тип — вектор (он зависит от значения — натурального числа). И вектор двух строк и вектор трех строк — разные типы. Еще примеры зависимых типов — ненулевое число, непустой список, пара чисел, где второе число меньше первого, тип-равенство 1 =:= 2
(у которого нет значений), типы 1 =:= 1
, 2 =:= 2
(у которых по одному значению) и т.д.
Так можно задать зависимый тип Ba
, который зависит от значений типа A
, и переменную этого типа:
val Ba = "B(_ : A)" :: A ->: Type
val b = "b" :: Ba(a)
Теперь про стрелочки. Есть 4 основных типа стрелок для функций: :->
, :~>
, ->:
, ~>:
. С двоеточиями слева — для лямбд (т.е. самих функций), с двоеточиями справа — для типов функций. С дефисами — для обычных функций, с тильдами — для зависимых функций (т.е. у которых не только значение, но и тип значения зависит от аргумента). В качестве примера — тождественная функция
val id = A :~> (a :-> a) !: A ~>: (A ->: A)
Часть проверки типов осуществляется в рантайме, но часть информации о типах видит и компилятор Скалы:
val f : FuncLike[Term, Term] = a :~> b !: a ~>: Ba(a)
val f : Term => Term = a :~> b !: a ~>: Ba(a)
Здесь зависимый функциональный тип из ProvingGround/HoTT компилятор Скалы видит как обычную функцию в Скале.
Можно задавать индуктивные типы [14]. Например, булев тип с конструкторами «истина» и «ложь»:
val Bool = "Boolean" :: Type
val BoolInd = ("true" ::: Bool) |: ("false" ::: Bool) =: Bool
val tru :: fls :: HNil = BoolInd.intros
то есть типичное задание индуктивного типа выглядит как
val идентификатор_объявления = (...) |: (...) |: (...) =: Имя_типа
где конструкторы значений этого типа отделены |:
.
Еще пример — тип натуральных чисел с конструкторами «ноль» и «следующее число за натуральным n
»:
val Nat = "Nat" :: Type
val NatInd = ("0" ::: Nat) |: ("succ" ::: Nat -->>: Nat) =: Nat
val zero :: succ :: HNil = NatInd.intros
val one = succ(zero) !: Nat
val two = succ(one) !: Nat
// ...
Тип целых чисел с конструкторами «плюс натуральное n
» и «минус натуральное n
минус 1» использует уже определенный тип натуральных чисел:
val Int = "Integer" :: Type
val IntInd = ("pos" ::: Nat ->>: Int) |: ("neg" ::: Nat ->>: Int) =: Int
val pos :: neg :: HNil = IntInd.intros
Тип списка значений типа A
имеет конструкторы «пустой список» и «список с головой типа A
и хвостом типа ListA
»:
val ListA = "List(A)" :: Type
val ListAInd = ("nil" ::: ListA) |: ("cons" ::: A ->>: ListA -->>: ListA) =: ListA
val nil :: cons :: HNil = ListAInd.intros
У типа бинарного дерева (для простоты без значений некоторого типа в узлах) есть конструкторы «лист» и «вилка» (второй принимает пару поддеревьев):
val BTree = "BTree" :: Type
val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: BTree -->>: BTree -->>: BTree) =: BTree
val leaf :: fork :: HNil = BTreeInd.intros
Альтернативно конструктор «вилка» могла бы принимать функцию, которая переводит ложь в одно поддерево, истину в другое:
val BTree = "BTree" :: Type
val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: (Bool -|>: BTree) -->>: BTree) =: BTree
val leaf :: fork :: HNil = BTreeInd.intros
Если тип зависимый (indexed inductive type [15]), например вектор Vec
или тип-равенство Id
, то надо использовать =::
вместо =:
, стрелку с тильдой и ссылаться на тип внутри конструкторов (Имя_типа -> Имя_типа(n))
в возвращаемом типе, (Имя_типа :> Имя_типа(n))
в принимаемом типе, а не просто Имя_типа(n)
. Например, тип вектора длины n
:
val VecA = "Vec(A)" :: Nat ->: Type
val n = "n" :: Nat
val VecAInd = ("nil" ::: (VecA -> VecA(zero) )) |:
{"cons" ::: n ~>>: (A ->>: (VecA :> VecA(n) ) -->>: (VecA -> VecA(succ(n)) ))} =:: VecA
val vnil :: vcons :: HNil = VecAInd.intros
Еще один полезный зависимый тип позволяет формализовать понятие натурального числа, не превышающего другое натуральное число:
val Fin = "Fin" :: Nat ->: Type
val FinInd = {"FZ" ::: n ~>>: (Fin -> Fin(succ(n)) )} |:
{"FS" ::: n ~>>: ((Fin :> Fin(n) ) -->>: (Fin -> Fin(succ(n)) ))} =:: Fin
val fz :: fs :: HNil = FinInd.intros
Действительно, нет способа сконструировать значение типа Fin(zero)
. Есть ровно одно значение типа Fin(one)
:
val fz0 = fz(zero) !: Fin(one)
Есть ровно два значения типа Fin(two)
:
val fz1 = fz(one) !: Fin(two)
val fs1 = fs(one)(fz0) !: Fin(two)
Есть ровно три значения типа Fin(three)
:
fz(two) !: Fin(three)
fs(two)(fz1) !: Fin(three)
fs(two)(fs1) !: Fin(three)
и т.д.
Несколько слов об отличии семейства индуктивных типов (family of inductive types) от индексированного индуктивного типа (indexed inductive type). Например, List(A)
— это семейство, а Vec(A)(n)
— это семейство относительно типа A
, но индексированный тип относительно натурального индекса n
. Индуктивный тип — это тип, конструкторы которого для «следующих» значений могут использовать «предыдущие» значения (как у типов Nat
, List
и т.д.). Vec(A)(n)
при фиксированном A
является индуктивным типом, но не является при фиксированном n
. В ProvingGround в настоящее время нет семейств индуктивных типов, т.е. нельзя, имея индуктивное определение, например, типа List(A)
, легко получить индуктивное определение типов List(B)
, List(Nat)
, List(Bool)
, List(List(A))
и т.д. Но можно эмулировать семейства с помощью индексированных типов:
val List = "List" :: Type ->: Type
val ListInd = {"nil" ::: A ~>>: (List -> List(A) )} |:
{"cons" ::: A ~>>: (A ->>: (List :> List(A) ) -->>: (List -> List(A) ))} =:: List
val nil :: cons :: HNil = ListInd.intros
cons(Nat)(zero)(cons(Nat)(one)(cons(Nat)(two)(nil(Nat)))) !: List(Nat) // список 0, 1, 2
и
val Vec = "Vec" :: Type ->: Nat ->: Type
val VecInd = {"nil" ::: A ~>>: (Vec -> Vec(A)(zero) )} |:
{"cons" ::: A ~>>: n ~>>: (A ->>: (Vec :> Vec(A)(n) ) -->>: (Vec -> Vec(A)(succ(n)) ))} =:: Vec
val vnil :: vcons :: HNil = VecInd.intros
vcons(Bool)(two)(tru)(vcons(Bool)(one)(fls)(vcons(Bool)(zero)(tru)(vnil(Bool)))) !: Vec(Bool)(succ(two))
// 3-элементный вектор tru, fls, tru
Можно также определить гетерогенный список (HList
):
val HLst = "HList" :: Type ->: Type
val HLstInd = {"nil" ::: A ~>>: (HLst -> HLst(A) )} |:
{"cons" ::: A ~>>: (A ->>: (B ~>>: ((HLst :> HLst(B) ) -->>: (HLst -> HLst(A) ))))} =:: HLst
val hnil :: hcons :: HNil = HLstInd.intros
Мы сейчас реализовали собственный HList
в библиотеке ProvingGround, которая написана поверх Shapeless, в которой основным строительным элементом является HList
.
В библиотеке можно эмулировать обобщенные алгебраические типы данных (GADT [16]). Код, который выглядит на Хаскеле
{-# Language GADTs #-}
data Expr a where
ELit :: a -> Expr a
ESucc :: Expr Int -> Expr Int
EIsZero :: Expr Int -> Expr Bool
EIf :: Expr Bool -> Expr a -> Expr a -> Expr a
и на чистой Скале
sealed trait Expr[A]
case class ELit[A](lit: A) extends Expr[A]
case class ESucc(num: Expr[Int]) extends Expr[Int]
case class EIsZero(num: Expr[Int]) extends Expr[Boolean]
case class EIf[A](cond: Expr[Boolean], thenExpr: Expr[A], elseExpr: Expr[A]) extends Expr[A]
запишется в ProvingGround как
val Expr = "Expr" :: Type ->: Type
val ExprInd = {"ELit" ::: A ~>>: (A ->>: (Expr -> Expr(A) ))} |:
{"ESucc" ::: Expr(Nat) ->>: (Expr -> Expr(Nat) )} |:
{"EIsZero" ::: Expr(Nat) ->>: (Expr -> Expr(Bool) )} |:
{"EIf" ::: A ~>>: (Expr(Bool) ->>: Expr(A) ->>: Expr(A) ->>: (Expr -> Expr(A) ))} =:: Expr
val eLit :: eSucc :: eIsZero :: eIf :: HNil = ExprInd.intros
Также можно в библиотеке эмулировать классы типов [17]. Например, функтор [18]:
val A = "A" :: Type
val B = "B" :: Type
val C = "C" :: Type
val Functor = "Functor" :: (Type ->: Type) ->: Type
val F = "F(_ : U_0)" :: Type ->: Type
val Fmap = A ~>: (B ~>: ((A ->: B) ->: (F(A) ->: F(B) )))
val FunctorInd = {"functor" ::: F ~>>: (Fmap ->>: (Functor -> Functor(F) ))} =:: Functor
val functor :: HNil = FunctorInd.intros
Можно, например, список объявить экземпляром (instance) функтора:
val as = "as" :: List(A)
val indList_map = ListInd.induc(A :~> (as :-> (B ~>: ((A ->: B) ->: List(B) )))) // это индукция, о рекурсии и индукции идет речь ниже
val mapas = "map(as)" :: B ~>: ((A ->: B) ->: List(B))
val f = "f" :: A ->: B
val map = indList_map(A :~> (B :~> (f :->
nil(B)
)))(A :~> (a :-> (as :-> (mapas :-> (B :~> (f :->
cons(B)(f(a))(mapas(B)(f))
)))))) !: A ~>: (List(A) ->: (B ~>: ((A ->: B) ->: List(B) )))
val listFunctor = functor(List)(A :~> (B :~> (f :-> (as :-> map(A)(as)(B)(f) )))) !: Functor(List)
Можно в класс типов добавить законы:
val fmap = "fmap" :: A ~>: (B ~>: ((A ->: B) ->: (F(A) ->: F(B) )))
val Fmap_id = A ~>: ( fmap(A)(A)(id(A)) =:= id(F(A)) )
val f = "f" :: A ->: B
val g = "g" :: B ->: C
val compose = A :~> (B :~> (C :~> (f :-> (g :-> (a :-> g(f(a))
))))) !: A ~>: (B ~>: (C ~>: ((A ->: B) ->: ((B ->: C) ->: (A ->: C)))))
val Fmap_compose = A ~>: (B ~>: (C ~>: (f ~>: (g ~>: (
fmap(A)(C)(compose(A)(B)(C)(f)(g)) =:= compose(F(A))(F(B))(F(C))(fmap(A)(B)(f))(fmap(B)(C)(g)) )))))
val FunctorInd = {"functor" ::: F ~>>: (fmap ~>>: (Fmap_id ->>: (Fmap_compose ->>: (Functor -> Functor(F) ))))} =:: Functor
val functor :: HNil = FunctorInd.intros
В библиотеке уже есть встроенные сигма-тип (тип зависимой пары), пи-тип (тип зависимой функции, мы его уже видели выше), тип-равенство (identity type):
mkPair(a, b) !: Sgma(a !: A, Ba(a))
one.refl !: (one =:= one)
one.refl !: IdentityTyp(Nat, one, one)
two.refl !: (two =:= two)
(one =:= two) !: Type
но можно определить и свой, например, тип-равенство:
val Id = "Id" :: A ~>: (A ->: A ->: Type)
val IdInd = ("refl" ::: A ~>>: a ~>>: (Id -> Id(A)(a)(a) )) =:: Id
val refl :: HNil = IdInd.intros
refl(Nat)(two) !: Id(Nat)(two)(two)
Типы-равенства естественно возникают, когда начинается разговор о соответствии Карри-Ховарда [19]. С одной стороны A ->: B
— это функции из A
в B
, с другой — это логическая формула «из утверждения A
следует B
». И, с одной стороны, (A ->: B) ->: A ->: B
— это тип функции высшего порядка, которая принимает на вход функцию A ->: B
и значение типа A
и возвращает эту функцию, примененную к этому значению, т.е. значение типа B
. С другой стороны, это правило вывода в логике modus ponens — «если верно, что из A
следует B
, и верно A
, то верно B
». С такой точки зрения типы — это утверждения, а значения типов — это доказательства этих утверждений. И утверждение верно, если соответствующий тип населен, т.е. существует значение этого типа. Логическое «и» соответствует произведению типов, логическое «или» — сумме типов, логическое «не» — типу A ->: Zero
, т.е. функциям в пустой тип. Так в теории типов возникает логика. Правда, не любая логика, а так называемая интуиционистская [20] или конструктивная, т.е. логика без закона исключения третьего. Действительно, вообще говоря, нельзя сконструировать значение типа PlusTyp(A, A ->: Zero)
(если не удалось доказать A
, то это еще не значит, что удалось доказать не-A
). Интересно, что справедливо отрицание к отрицанию закона исключения третьего:
val g = "g" :: PlusTyp(A, A ->: Zero) ->: Zero
val g1 = a :-> g(PlusTyp(A, A ->: Zero).incl1(a)) !: A ->: Zero
g :-> g(PlusTyp(A, A ->: Zero).incl2(g1)) !: (PlusTyp(A, A ->: Zero) ->: Zero) ->: Zero
Ну так вот, если типы — утверждения, а значения типов — доказательства, то раз равенство двух термов a1 =:= a2
— это утверждение, значит и тип. Тип зависимый, т.к. зависит от значений a1, a2
некоторого типа A
. Если a1, a2
разные, то не должно быть способа сконструировать значение этого типа, т.к. утверждение ложно. Если одинаковые, то наоборот должен быть способ сконструировать значение, раз утверждение верно, так что у нашего индуктивного типа единственный конструктор refl(A)(a) !: Id(A)(a)(a)
(или a.refl !: (a =:= a)
для встроенного типа-равенства).
Еще один полезный тип при доказательстве теорем с неравенствами:
val LTE = "≤" :: Nat ->: Nat ->: Type
val LTEInd = {"0 ≤ _" ::: m ~>>: (LTE -> LTE(zero)(m) )} |:
{"S _ ≤ S _" ::: n ~>>: m ~>>: ((LTE :> LTE(n)(m) ) -->>: (LTE -> LTE(succ(n))(succ(m)) ))} =:: LTE
val lteZero :: lteSucc :: HNil = LTEInd.intros
Еще в библиотеке можно работать с высшими индуктивными типами [21]. Например, окружностью
val Circle = "S^1" :: Type
val base = "base" :: Circle // конструктор
val loop = "loop" :: (base =:= base) // еще один конструктор
и сферой
val Sphere = "S^2" :: Type
val base = "base" :: Sphere // конструктор
val surf = "surf" :: (base.refl =:= base.refl) // еще один конструктор
// val surf = "surf" :: IdentityTyp(base =:= base, base.refl, base.refl)
// val surf = "surf" :: IdentityTyp(IdentityTyp(Sphere, base, base), base.refl, base.refl)
Теперь о том, как определять (рекурсивные) функции. Библиотека для каждого индуктивного типа генерирует методы .rec
, .induc
, т.е. рекурсию (aka рекурсор) и индукцию — элиминаторы в постоянный и зависимый тип соответственно, с помощью которых можно осуществлять сопоставление с образцом (pattern matching), если надо — рекурсивное. Например, можно определить логическое «не»:
val b = "b" :: Bool
val recBB = BoolInd.rec(Bool)
val not = recBB(fls)(tru)
Здесь можно считать, что мы сделали сопоставление с образцом:
match {
case true => false
case false => true
}
Проверяем, что всё работает:
not(tru) == fls
not(fls) == tru
Также можно определить логическое «и»:
val recBBB = BoolInd.rec(Bool ->: Bool)
val and = recBBB(b :-> b)(b :-> fls)
Здесь можно считать, что мы сделали сопоставление с образцом по первому аргументу:
// псевдокод
match {
case true => (b => b)
case false => (b => false)
}
Проверяем:
and(fls)(tru) == fls
and(tru)(tru) == tru
Можно определить удваивание натурального числа:
val n = "n" :: Nat
val m = "m" :: Nat
val recNN = NatInd.rec(Nat)
val double = recNN(zero)(n :-> (m :-> succ(succ(m)) ))
Здесь опять можно считать, что мы сделали сопоставление с образцом:
// псевдокод
match {
case Zero => Zero
case Succ(n) =>
val m = double(n)
m + 2
}
Проверяем:
println(double(two).fansi)
> succ(succ(succ(succ(0))))
Определим сложение натуральных чисел:
val recNNN = NatInd.rec(Nat ->: Nat)
val addn = "add(n)" :: Nat ->: Nat
val add = recNNN(m :-> m)(n :-> (addn :-> (m :-> succ(addn(m)) )))
Здесь аналогично можно считать, что мы сделали сопоставление с образцом по первому аргументу:
// псевдокод
match {
case Zero => (m => m)
case Succ(n) =>
val addn = add(n)
m => addn(m) + 1
}
Проверка:
println(add(two)(three).fansi)
> succ(succ(succ(succ(succ(0)))))
Определим также конкатенацию векторов:
val vn = "v_n" :: VecA(n)
val vm = "v_m" :: VecA(m)
val indVVV = VecAInd.induc(n :~> (vn :-> (m ~>: (VecA(m) ->: VecA(add(n)(m)) ))))
val concatVn = "concat(v_n)" :: (m ~>: (VecA(m) ->: VecA(add(n)(m)) ))
val vconcat = indVVV(m :~> (vm :-> vm))(n :~> (a :-> (vn :-> (concatVn :-> (m :~> (vm :->
vcons(add(n)(m))(a)(concatVn(m)(vm)) ))))))
Здесь мы используем не рекурсию, а индукцию, т.к. нам нужен элиминатор в зависимый тип
m ~>: (VecA(m) ->: VecA(add(n)(m)))
— действительно, этот тип зависит от n
из вектора (первый аргумент конкатенации), который мы деконструируем при сопоставлении с образцом:
// псевдокод
match {
case (Zero, Nil) => (vm => vm)
case (Succ(n), Cons(a)(vn)) =>
val concatVn = concat(vn)
vm => Cons(a)(concatVn(vm))
}
Тестируем:
val a = "a" :: A
val a1 = "a1" :: A
val a2 = "a2" :: A
val a3 = "a3" :: A
val a4 = "a4" :: A
val vect = vcons(one)(a)(vcons(zero)(a1)(vnil))
val vect1 = vcons(two)(a2)(vcons(one)(a3)(vcons(zero)(a4)(vnil)))
println(vconcat(two)(vect)(three)(vect1).fansi)
> cons(succ(succ(succ(succ(0)))))(a)(cons(succ(succ(succ(0))))(a1)(cons(succ(succ(0)))(a2)(cons(succ(0))(a3)(cons(0)(a4)(nil)))))
Покажу еще пример, как теоремы доказываются в ProvingGround. Докажем, что add(n)(n) =:= double(n)
.
val indN_naddSm_eq_S_naddm = NatInd.induc(n :-> (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )))
val hyp1 = "n+Sm=S(n+m)" :: (m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) ))
val lemma = indN_naddSm_eq_S_naddm(m :~> succ(m).refl)(n :~> (hyp1 :-> (m :~>
IdentityTyp.extnslty(succ)( add(n)(succ(m)) )( succ(add(n)(m)) )( hyp1(m) )
))) !: n ~>: m ~>: ( add(n)(succ(m)) =:= succ(add(n)(m)) )
val lemma1 = IdentityTyp.extnslty(succ)( add(n)(succ(n)) )( succ(add(n)(n)) )( lemma(n)(n) )
val indN_naddn_eq_2n = NatInd.induc(n :-> ( add(n)(n) =:= double(n) ))
val hyp = "n+n=2*n" :: ( add(n)(n) =:= double(n) )
val lemma2 = IdentityTyp.extnslty( m :-> succ(succ(m)) )( add(n)(n) )( double(n) )(hyp)
indN_naddn_eq_2n(zero.refl)(n :~> (hyp :->
IdentityTyp.trans(Nat)( add(succ(n))(succ(n)) )( succ(succ(add(n)(n))) )( double(succ(n)) )(lemma1)(lemma2)
)) !: n ~>: ( add(n)(n) =:= double(n) )
Окружность не получается определить как обычный индуктивный тип через (...) |: (...) =:: ...
(действительно, конструктор loop
возвращает не значение типа Circle
, как было бы для обычного индуктивного типа). Поэтому и рекурсию с индукцией приходится определять вручную:
val recCirc = "rec_{S^1}" :: A ~>: a ~>: (a =:= a) ->: Circle ->: A
val B = "B(_ : S^1)" :: Circle ->: Type
val b = "b" :: B(base)
val c = "c" :: Circle
val indCirc = "ind_{S^1}" :: B ~>: b ~>: (( IdentityTyp.transport(B)(base)(base)(loop)(b) =:= b ) ->: c ~>: B(c) )
с двумя аксиомами comp_base
и comp_loop
:
val l = "l" :: ( IdentityTyp.transport(B)(base)(base)(loop)(b) =:= b )
val comp_base = "comp_base" :: B ~>: b ~>: l ~>: ( indCirc(B)(b)(l)(base) =:= b )
val P = "P(_ : A)" :: A ->: Type
val f = "f" :: a ~>: P(a)
val dep_map = "dep_map" :: A ~>: (P ~>: (f ~>: (a ~>: (a1 ~>: (( a =:= a1 ) ->: ( f(a) =:= f(a1) )))))) // dep_map аналогично IdentityTyp.extnslty(f), но для зависимой f
val comp_loop = "comp_loop" :: B ~>: b ~>: l ~>: ( dep_map(Circle)(B)(indCirc(B)(b)(l))(base)(base)(loop) =:= l )
Несколько слов о том, как запускать код на ProvingGround. Есть 3 способа.
ProvingGround/mantle/target/web/classes/test
).
sbt server/run
и затем открыть в браузере http://localhost:8080 [25].
ProvingGround/core
. Для этого нужно положить новый build.sbt [27] сюда: ProvingGround/core/build.sbt
.
Список импортов:
import provingground._
import HoTT._
import TLImplicits._
import shapeless._
//import ammonite.ops._
import FansiShow._
Если кому интересна эта тема (теория типов, гомотопическая теория типов, зависимые типы, вычисления на уровне типов, автоматическое доказательство теорем), добро пожаловать на мой курс [28]. Он вводный. По HoTT скорее даже не введение, а введение во введение, но по остальным направлениям, думаю, дотягивает до уровня просто введения. Спасибо за внимание.
Автор: dmitrymitin
Источник [29]
Сайт-источник PVSM.RU: https://www.pvsm.ru
Путь до страницы источника: https://www.pvsm.ru/matematika/255834
Ссылки в тексте:
[1] ProvingGround: https://github.com/siddhartha-gadgil/ProvingGround
[2] Shapeless: https://github.com/milessabin/shapeless
[3] документация: http://siddhartha-gadgil.github.io/ProvingGround/
[4] Сиддхартха Гаджил: http://math.iisc.ernet.in/~gadgil/
[5] HoTT: https://homotopytypetheory.org/book/
[6] курс: http://compsciclub.ru/courses/idrisprogramming/2017-spring/
[7] другая: http://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types
[8] path-dependent типов: http://danielwestheide.com/blog/2013/02/13/the-neophytes-guide-to-scala-part-13-path-dependent-types.html
[9] type-level: http://slick.lightbend.com/talks/scalaio2014/Type-Level_Computations.pdf
[10] имплицитов: http://docs.scala-lang.org/tutorials/tour/implicit-parameters.html
[11] отличия: https://www.youtube.com/watch?v=R8GksuRw3VI
[12] «Aux» паттерна: http://gigiigig.github.io/posts/2015/09/13/aux-pattern.html
[13] Зависимый тип: https://en.wikipedia.org/wiki/Dependent_type
[14] индуктивные типы: https://en.wikipedia.org/wiki/Inductive_type
[15] indexed inductive type: https://ncatlab.org/nlab/show/inductive+family
[16] GADT: https://en.wikibooks.org/wiki/Haskell/GADT
[17] классы типов: https://en.wikipedia.org/wiki/Type_class
[18] функтор: https://wiki.haskell.org/Functor
[19] соответствии Карри-Ховарда: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
[20] интуиционистская: https://ru.wikipedia.org/wiki/%D0%98%D0%BD%D1%82%D1%83%D0%B8%D1%86%D0%B8%D0%BE%D0%BD%D0%B8%D0%B7%D0%BC
[21] высшими индуктивными типами: https://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/
[22] Ammonite REPL: http://www.lihaoyi.com/Ammonite/#Ammonite-REPL
[23] sbt: http://www.scala-sbt.org/
[24] github.com/siddhartha-gadgil/ProvingGround.git: https://github.com/siddhartha-gadgil/ProvingGround.git
[25] http://localhost:8080: http://localhost:8080
[26] модификации: https://github.com/siddhartha-gadgil/ProvingGround/issues/124
[27] новый build.sbt: https://stepik.org/media/attachments/course/2294/build.sbt
[28] мой курс: https://stepik.org/2294
[29] Источник: https://habrahabr.ru/post/329176/?utm_source=habrahabr&utm_medium=rss&utm_campaign=sandbox
Нажмите здесь для печати.