それはすべて、StepikaコンテストのRockで依存型に関する入門コースを記録したかったという事実から始まりました。 繰り返したくありませんでしたが、最近、イドリスに良いコースが登場しました。 Scalaは、最も一般的な関数型言語の1つとして選ばれました。 「Scala」、「dependent types」、「HoTT」および最も有望な外観のProvingGroundに従ってgithubでGoogleを検索しました。 すぐに免責事項-特定の言語やライブラリが、依存型を使用したプログラミング、自動定理の証明、HoTTの操作に最も適しているとは主張しません。 他の言語やライブラリを使用することもできます-別のコースがあります。
ご存じのように、Scalaは依存型のサポートが制限されている言語です。 依存型は、 パス依存型 、 型レベル値、および含意を使用して実装されます（ 別の観点がエミュレートされます）。 ベアロックまたはロックプラスシェイプレスの依存型を説明し、型パラメーター（ジェネリック）からの型メンバーの違い 、含意、パス依存型、 「補助」パターン 、型レベルの計算などの技術的詳細に行き詰まります。 私は本当にしたくありませんでした。 したがって、コースの一部はむき出しのロックで行われましたが、練習のほとんどはProvingGroundで行われました。
用語と種類
変数、用語、タイプ、関数などを設定するには ProvingGroundはDSLを提供します。
したがって、タイプ
A
とこのタイプの変数を宣言できます。
val A = "A" :: Type val a = "a" :: A
つまり 典型的な広告は次のようになります
val _ = " " :: _
.fansi
メソッドを使用して「美しく」という用語を
.fansi
し、
.fansi
を使用してそのタイプを印刷でき
.fansi
。
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
はScalaのタイプです。
そのため、変数を設定した場合、
::
後に型を記述し、すでに用語がある場合は、その型を
!:
確認でき
!:
a !: A
この行がコンパイルされているという事実は、タイプが正しく指定されていることを意味します。
依存型
タイプを少し思い出してください。 値があり、タイプがあります。 各値にはタイプがあります。 依存型は、値依存型 （別の型の）です。 たとえば、2行のリストと3行のリストは、同じタイプの値（行のリスト）です。 しかし、要素の数に関する情報を型レベルに渡すと、従属型-ベクトル（値に依存-自然数）が得られます。 また、2行のベクトルと3行のベクトルは異なるタイプです。 依存型の他の例としては、ゼロ以外の数値、空でないリスト、2番目の数値が最初の数値より小さい数値のペア、等値タイプ
1 =:= 2
（値なし）、タイプ
1 =:= 1
2 =:= 2
（これ1つの値）など
したがって、タイプ
A
の値とこのタイプの変数に依存する依存タイプ
Ba
設定できます。
val Ba = "B(_ : A)" :: A ->: Type val b = "b" :: Ba(a)
機能
次に矢印について。 機能の矢印には、主に4つのタイプがあり
~>:
->:
~>:
、
->:
~>:
左側にコロンを-ラムダ（つまり関数自体）に、右側にコロンを-関数のタイプに。 ハイフンを使用-通常の関数の場合、チルダを使用-依存関数の場合（つまり、値だけでなく値のタイプも引数に依存します）。 例として、同一の機能
val id = A :~> (a :-> a) !: A ~>: (A ->: A)
型チェックの一部は実行時に行われますが、Scalaコンパイラーは型情報の一部も確認します。
val f : FuncLike[Term, Term] = a :~> b !: a ~>: Ba(a) val f : Term => Term = a :~> b !: a ~>: Ba(a)
ここでは、RockのProvingGround / HoTTコンパイラの従属関数タイプは、Rockの通常の関数と見なしています。
誘導型
誘導タイプを指定できます。 たとえば、コンストラクターが「true」および「false」であるブール型：
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 // ...
コンストラクター「plus integer
n
」および「minus integer
n
minus 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
バイナリツリータイプ（簡単にするため、ノードに特定のタイプの値を持たない）には、コンストラクター「リーフ」と「フォーク」があります（2番目はサブツリーのペアを取ります）。
val BTree = "BTree" :: Type val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: BTree -->>: BTree -->>: BTree) =: BTree val leaf :: fork :: HNil = BTreeInd.intros
あるいは、プラグコンストラクターは、嘘を1つのサブツリーに変換し、真実を別のサブツリーに変換する関数を取ることができます。
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)
型の値は1つだけです
Fin(one)
。
val fz0 = fz(zero) !: Fin(one)
タイプ
Fin(two)
値は正確に2つあります。
val fz1 = fz(one) !: Fin(two) val fs1 = fs(one)(fz0) !: Fin(two)
タイプ
Fin(three)
値は正確に3つあります。
fz(two) !: Fin(three) fs(two)(fz1) !: Fin(three) fs(two)(fs1) !: Fin(three)
など
誘導型ファミリー
帰納的タイプのファミリーとインデックス付きの帰納的タイプの違いについてのいくつかの言葉。 たとえば、
List(A)
はファミリであり、
Vec(A)(n)
はタイプ
A
に関連するファミリですが、インデックス付きタイプは自然インデックス
n
ます。 帰納的型は、コンストラクタが「次の」値に「前の」値を使用できる型です（
Nat
、
List
などの型と同様）。 固定
A
Vec(A)(n)
は誘導型ですが、固定
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ライブラリに独自の
HList
を実装しました。これはShapelessの上に記述されており、メインの構築要素は
HList
です。
代数データ型
ライブラリは、一般化された代数データ型（ GADT ）をエミュレートできます。 Haskellコード
{-# 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
型クラス
ライブラリで型クラスをエミュレートすることもできます。 たとえば、 ファンクター ：
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
平等タイプ
ライブラリには、組み込みのシグマ型（依存ペアの型）、pi型（依存関数の型、上で既に見た）、ID型が既にあります。
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
への関数であり、他方では、「fromステートメント
A
は
B
続く」という論理式です。 そして、一方で、
(A ->: B) ->: A ->: B
は、入力関数
A ->: B
およびタイプ
A
値を受け取り、それに適用されるこの関数を返す高階関数のタイプです。値、つまり タイプ
B
値
B
一方、これは、法則ポネンスロジックの推論規則です。「
A
が
A
から続き、
A
が真である場合、
B
は真です。」 この観点から、タイプはステートメントであり、タイプ値はこれらのステートメントの証拠です。 そして、対応するタイプが入力されている場合、つまり このタイプの値があります。 論理「and」は型の積に、論理「or」は型の合計に、論理「not」は型
A ->: Zero
に対応します。 空の型に機能します。 したがって、型理論には論理があります。 真実ではなく、論理ではなく、いわゆる直観主義的または建設的、すなわち 第三の排除の法則のない論理。 実際、一般的に言えば、
PlusTyp(A, A ->: Zero)
型の値を構築することはできません
PlusTyp(A, A ->: Zero)
（
A
を証明できなかった場合、これは
PlusTyp(A, A ->: Zero)
を証明できたという意味ではありません）。 興味深いことに、3番目の排除法の否定は真実です。
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
タイプがステートメントであり、タイプの値が証明である場合、2つの用語
a1 =:= a2
の等価性はステートメントであるため、タイプを意味します。 タイプが依存しているのは、 タイプ
A
値
a1, a2
依存します
A
a1, a2
異なる場合、このタイプの値を構築する方法はないはずです。 ステートメントは偽です。 それらが同じ場合、反対に、ステートメントがtrueであるため、値を構築する方法があるはずです。そのため、誘導型にはコンストラクター
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)
再帰と帰納
（再帰）関数を定義する方法について説明します。 各帰納的タイプのライブラリは、
.induc
、
.induc
、つまり 再帰（別名再帰）および誘導-定数および依存型へのエリミネーター。それぞれ、必要に応じて再帰的にパターンマッチングを実行できます。 たとえば、論理的な「not」を定義できます。
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
論理的な「and」も定義できます。
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
自然数の2倍を決定できます。
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) )
2つの公理
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つの方法があります。
- 最初の推奨事項-コンソールから（ Ammonite REPLをロードして）コマンドを使用して
sbt mantle / test：実行します （ github.com/siddhartha-gadgil/ProvingGround.gitリポジトリを複製した後、ProvingGroundプロジェクトのルートから、Ammonite REPLの起動に失敗した場合、空のディレクトリProvingGround/mantle/target/web/classes/test
）。
- 2番目は、
sbt server/run
コマンドを使用してから、ブラウザーでhttp：// localhost：8080を開きます 。
- 3番目はIDEからのものです。 IntelliJ Idea 2017.1.3では、build.sbtの変更後にプロジェクトがインポートされる場合がありますが、コードが起動しない場合があります。 解決策は、プロジェクト全体ではなく、
ProvingGround/core
サブプロジェクトのみをIdeaにインポートすることです。 これを行うには、 新しいbuild.sbtをProvingGround/core/build.sbt
ます。
インポートのリスト：
import provingground._ import HoTT._ import TLImplicits._ import shapeless._ //import ammonite.ops._ import FansiShow._
このトピック（型理論、ホモトピー型理論、依存型、型レベル計算、定理の自動証明）に興味がある人は、私のコースへようこそ。 彼は入門です。 HoTTによれば、それはおそらく序論ではなく、序論への序論ですが、他の分野では、序論のレベルに達していると思います。 ご清聴ありがとうございました。