Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.
Началось все с того, что мне захотелось записать вводный курс по зависимым типам на Скале для конкурса Степика. Не хотелось повторяться, на Идрисе недавно появился хороший курс. Скала была выбрана как один из самых популярных функциональных языков. Погуглил по гитхабу по словам «Скала», «зависимые типы», «HoTT» и наиболее многообещающе выглядела ProvingGround. Сразу дисклеймер — я не утверждаю, что те или иные языки или библиотеки наиболее подходят для программирования с зависимыми типами, автоматического доказательства теорем, работы с HoTT. Можно было взять другие языки или библиотеки — был бы другой курс.
Как известно, Скала — язык с ограниченной поддержкой зависимых типов. Зависимые типы имплементируются в ней (другая точка зрения — эмулируются) с помощью path-dependent типов, type-level значений и имплицитов. Объяснять зависимые типы на голой Скале или Скале плюс Shapeless и погрязнуть в технических деталях типа отличия type members от type parameters (дженериков), имплицитов, path-dependent типов, «Aux» паттерна, type-level вычислений и т.д. не очень хотелось. Поэтому часть курса была на голой Скале, но бОльшая часть практики — на ProvingGround.
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
1 =:= 2
(у которого нет значений), типы 1 =:= 1
, 2 =:= 2
(у которых по одному значению) и т.д.Ba
, который зависит от значений типа A
, и переменную этого типа:val Ba = "B(_ : A)" :: A ->: Type
val b = "b" :: Ba(a)
:->
, :~>
, ->:
, ~>:
. С двоеточиями слева — для лямбд (т.е. самих функций), с двоеточиями справа — для типов функций. С дефисами — для обычных функций, с тильдами — для зависимых функций (т.е. у которых не только значение, но и тип значения зависит от аргумента). В качестве примера — тождественная функция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)
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
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)
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
.{-# 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]
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
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
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
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)
A ->: B
— это функции из A
в B
, с другой — это логическая формула «из утверждения A
следует B
». И, с одной стороны, (A ->: B) ->: A ->: B
— это тип функции высшего порядка, которая принимает на вход функцию A ->: B
и значение типа A
и возвращает эту функцию, примененную к этому значению, т.е. значение типа B
. С другой стороны, это правило вывода в логике modus ponens — «если верно, что из A
следует B
, и верно A
, то верно B
». С такой точки зрения типы — это утверждения, а значения типов — это доказательства этих утверждений. И утверждение верно, если соответствующий тип населен, т.е. существует значение этого типа. Логическое «и» соответствует произведению типов, логическое «или» — сумме типов, логическое «не» — типу A ->: Zero
, т.е. функциям в пустой тип. Так в теории типов возникает логика. Правда, не любая логика, а так называемая интуиционистская или конструктивная, т.е. логика без закона исключения третьего. Действительно, вообще говоря, нельзя сконструировать значение типа 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
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)))))
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/mantle/target/web/classes/test
).sbt server/run
и затем открыть в браузере http://localhost:8080.ProvingGround/core
. Для этого нужно положить новый build.sbt сюда: ProvingGround/core/build.sbt
.import provingground._
import HoTT._
import TLImplicits._
import shapeless._
//import ammonite.ops._
import FansiShow._
К сожалению, не доступен сервер mySQL