From dependent types to homotopic type theory on Scala + Shapeless + ProvingGround

Hello. I want to share my experience using the ProvingGround library written on Rock using Shapeless . The library has documentation , though not very extensive. The author of the library is Siddhartha Hajil from the Indian Institute of Science. The library is experimental. Siddhartha himself says that this is not a library yet, but “work in progress”. The global goal of the library is to take an article from a living mathematician, parse the text, translate natural language with formulas into formal proofs that the compiler could check. It is clear that this is still very far away. So far, the library can work with dependent types and the basics of the homotopy type theory ( HoTT ), (semi-) automatically proving theorems.

It all started with the fact that I wanted to record an introductory course on dependent types on the Rock for the Stepic competition. I did not want to repeat myself; a good course had recently appeared on Idris. Scala was chosen as one of the most popular functional languages. Googled by githab according to "Scala", "dependent types", "HoTT" and looked most promisingly ProvingGround. Immediately a disclaimer - I do not claim that certain languages ​​or libraries are most suitable for programming with dependent types, automatic proof of theorems, work with HoTT. It was possible to take other languages ​​or libraries - there would be a different course.

As is known, Scala is a language with limited support for dependent types. Dependent types are implemented in it ( another point of view is emulated) with the help of path-dependent types , type-level values ​​and implications . Explain dependent types on bare Rock or Rock plus Shapeless and get bogged down in the technical details of the type members difference from type parameters, implicates, path-dependent types, “Aux” patterns , type-level calculations, etc. didn't really want to. Therefore, part of the course was on bare Rock, but most of the practice was on ProvingGround.

Terms and types

To set variables, terms, types, functions, etc. ProvingGround provides its DSL .
So you can declare type A and variable a this type:
')

 val A = "A" :: Type val a = "a" :: A 

those. typical ad looks like

 val _ = "  " :: _ 

The term “beautifully” can be printed using the .fansi method, its type can be .typ using the .typ :

 println(a) > a : (A : U_0) println(a.fansi) > a println(a.typ) > A : U_0 println(a.typ.fansi) > A 

You can set the variable in more detail:

 val a : Term = "a" :: A 

Here A is the type in the ProvingGround library, i.e. HoTT is a type, and Term is a type in Scala.

So, if we set a variable, then we write the type after :: , and if we already have a term, then we can check its type using !:

 a !: A 

The fact that this line is compiled means that the type is specified correctly.

Dependent types

A small reminder of the types. There are values ​​and there are types. Each value has its type. A dependent type is a type that is dependent on a value (of another type). For example, a list of two lines and a list of three lines are values ​​of the same type — a list of lines. But if we take the information about the number of elements to the level of type, then we get a dependent type - a vector (it depends on the value - a natural number). Both the vector of two lines and the vector of three lines are different types. Other examples of dependent types are a non-zero number, a non-empty list, a pair of numbers where the second number is less than the first, equality type 1 =:= 2 (which has no values), types 1 =:= 1 , 2 =:= 2 (in which by one value), etc.

So you can set the dependent type of Ba , which depends on the values ​​of type A , and a variable of this type:

 val Ba = "B(_ : A)" :: A ->: Type val b = "b" :: Ba(a) 

Functions

Now, about the arrows. There are 4 main types of arrows for functions:: :-> :~> , ->: ~>: With colons on the left - for lambdas (ie, the functions themselves), with colons on the right - for types of functions. With hyphens - for ordinary functions, with tildes - for dependent functions (that is, for which not only the value, but also the type of the value depends on the argument). As an example, the identity function

 val id = A :~> (a :-> a) !: A ~>: (A ->: A) 

Part of type checking is done in runtime, but the Scala compiler also sees some type information:

 val f : FuncLike[Term, Term] = a :~> b !: a ~>: Ba(a) val f : Term => Term = a :~> b !: a ~>: Ba(a) 

Here the dependent functional type from the ProvingGround / HoTT compiler Scales sees as an ordinary function in Scala.

Inductive types

You can set inductive types . For example, Boolean type with constructors "true" and "false":

 val Bool = "Boolean" :: Type val BoolInd = ("true" ::: Bool) |: ("false" ::: Bool) =: Bool val tru :: fls :: HNil = BoolInd.intros 

that is, a typical inductive type assignment looks like

 val _ = (...) |: (...) |: (...) =: _ 

where value constructors of this type are separated by |:

Another example is the type of natural numbers with the constructors "zero" and "the next number after the natural 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 // ... 

The type of integers with the constructors “plus a positive integer n ” and “minus positive integer n minus 1” uses the already defined type of positive integers:

 val Int = "Integer" :: Type val IntInd = ("pos" ::: Nat ->>: Int) |: ("neg" ::: Nat ->>: Int) =: Int val pos :: neg :: HNil = IntInd.intros 

The type A value list type has “empty list” and “list with type A head and ListA type ListA ” ListA :

 val ListA = "List(A)" :: Type val ListAInd = ("nil" ::: ListA) |: ("cons" ::: A ->>: ListA -->>: ListA) =: ListA val nil :: cons :: HNil = ListAInd.intros 

The type of a binary tree (for simplicity, without values ​​of some type in nodes) has the constructors “leaf” and “fork” (the second accepts a couple of subtrees):

 val BTree = "BTree" :: Type val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: BTree -->>: BTree -->>: BTree) =: BTree val leaf :: fork :: HNil = BTreeInd.intros 

Alternatively, the constructor "fork" could take a function that translates a lie into one subtree, the truth into another:

 val BTree = "BTree" :: Type val BTreeInd = ("leaf" ::: BTree) |: ("fork" ::: (Bool -|>: BTree) -->>: BTree) =: BTree val leaf :: fork :: HNil = BTreeInd.intros 

Dependent Inductive Types

If the type is dependent ( indexed inductive type ), for example, Vec vector or equality type Id , then you should use =:: instead of =: arrow with a tilde and refer to the type inside constructors (_ -> _(n)) in the returned type, (_ :> _(n)) in the received type, not just _(n) . For example, the type of vector of length 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 

Another useful dependent type allows us to formalize the concept of a natural number that does not exceed another natural number:

 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 

Indeed, there is no way to construct a value of type Fin(zero) . There is exactly one Fin(one) value:

 val fz0 = fz(zero) !: Fin(one) 

There are exactly two Fin(two) values:

 val fz1 = fz(one) !: Fin(two) val fs1 = fs(one)(fz0) !: Fin(two) 

There are exactly three Fin(three) values:

 fz(two) !: Fin(three) fs(two)(fz1) !: Fin(three) fs(two)(fs1) !: Fin(three) 

etc.

Inductive type families

A few words about the difference between the family of inductive types (family of inductive types) from the indexed inductive type (indexed inductive type). For example, List(A) is a family, and Vec(A)(n) is a family with respect to type A , but an indexed type with respect to the natural index n . An inductive type is a type whose constructors for “next” values ​​can use “previous” values ​​(as with types Nat , List , etc.). Vec(A)(n) with fixed A is inductive type, but is not with fixed n . There are currently no inductive type families in ProvingGround, i.e. it is impossible, having an inductive definition, for example, of the type List(A) , it is easy to obtain an inductive definition of the types List(B) , List(Nat) , List(Bool) , List(List(A)) , etc. But you can emulate families using indexed types:

 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 

and

 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 

You can also define a heterogeneous list ( 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 

We have now implemented our own HList in the ProvingGround library, which is written on top of Shapeless, in which the main building HList is HList .

Algebraic data types

In the library, you can emulate generalized algebraic data types ( GADT ). Code that looks like 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 

and on a clean rock

 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] 

will be written to ProvingGround as

 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 

Type Classes

You can also emulate type classes in the library. For example, the functor :

 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 

You can, for example, declare a list as an instance of a functor:

 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) 

You can add laws to the type class:

 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 

Equality Types

The library already has built-in sigma-type (type of dependent pair), pi-type (type of dependent function, we have already seen it above), type-equality (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 

but you can define your own, for example, type-equality:

 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) 

Equality types naturally occur when the Curry-Howard correspondence begins. On the one hand, A ->: B is a function from A to B , on the other hand, it is a logical formula “from Statement A follows B ”. And, on the one hand, (A ->: B) ->: A ->: B is a type of higher order function that takes as input the function A ->: B and a value of type A and returns this function applied to this value, i.e. value of type B On the other hand, this is an inference rule in modus ponens logic - “if it is true that A follows from A , and A is true, then B is true”. From this point of view, types are statements, and type values ​​are proofs of these statements. And the statement is true if the corresponding type is populated, i.e. There is a value of this type. The logical “and” corresponds to the product of types, the logical “or” to the sum of the types, the logical “not” to the type A ->: Zero , i.e. functions in an empty type. So in the theory of types logic arises. True, not any logic, but the so-called intuitionistic or constructive, i.e. logic without the law of elimination of the third. Indeed, generally speaking, one cannot construct a value of type PlusTyp(A, A ->: Zero) (if one could not prove A , then this does not mean that one could prove non- A ). Interestingly, the negation to the negation of the law of excluding the third is true:

 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 

Well, if types are statements, and type values ​​are proofs, then the equality of two terms a1 =:= a2 is a statement, which means type. Type dependent, since depends on the values ​​of a1, a2 some type A If a1, a2 different, then there should not be a way to construct a value of this type, since the statement is false. If they are the same, then there should be a way to construct a value, since the statement is true, so our inductive type has a single constructor refl(A)(a) !: Id(A)(a)(a) (or a.refl !: (a =:= a) for the built-in equality type).

Another useful type in proving theorems with inequalities:

 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 

Higher inductive types

Even in the library, you can work with higher inductive types . For example, a circle

 val Circle = "S^1" :: Type val base = "base" :: Circle //  val loop = "loop" :: (base =:= base) //    

and sphere

 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) 

Recursion and induction

Now how to define (recursive) functions. The library for each inductive type generates methods .rec , .induc , i.e. recursion (aka recursor) and induction are eliminators into a permanent and dependent type, respectively, with which you can carry out pattern matching (pattern matching), if necessary - recursive. For example, you can define a logical "not":

 val b = "b" :: Bool val recBB = BoolInd.rec(Bool) val not = recBB(fls)(tru) 

Here we can assume that we have done pattern matching:

 match { case true => false case false => true } 

We check that everything works:

 not(tru) == fls not(fls) == tru 

You can also define a logical "and":

 val recBBB = BoolInd.rec(Bool ->: Bool) val and = recBBB(b :-> b)(b :-> fls) 

Here we can assume that we have made a comparison with the sample of the first argument:

 //  match { case true => (b => b) case false => (b => false) } 

Checking:

 and(fls)(tru) == fls and(tru)(tru) == tru 

You can determine the doubling of the natural number:

 val n = "n" :: Nat val m = "m" :: Nat val recNN = NatInd.rec(Nat) val double = recNN(zero)(n :-> (m :-> succ(succ(m)) )) 

Here again, we can assume that we have done pattern matching:

 //  match { case Zero => Zero case Succ(n) => val m = double(n) m + 2 } 

Checking:

 println(double(two).fansi) > succ(succ(succ(succ(0)))) 

Define the addition of natural numbers:

 val recNNN = NatInd.rec(Nat ->: Nat) val addn = "add(n)" :: Nat ->: Nat val add = recNNN(m :-> m)(n :-> (addn :-> (m :-> succ(addn(m)) ))) 

Here, similarly, we can assume that we have made a comparison with the sample in the first argument:

 //  match { case Zero => (m => m) case Succ(n) => val addn = add(n) m => addn(m) + 1 } 

Check:

 println(add(two)(three).fansi) > succ(succ(succ(succ(succ(0))))) 

We also define the concatenation of vectors:

 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)) )))))) 

Here we use not recursion, but induction, since we need an eliminator to a dependent type
m ~>: (VecA(m) ->: VecA(add(n)(m))) - indeed, this type depends on n from the vector (the first concatenation argument), which we deconstruct when comparing with the pattern:

 //  match { case (Zero, Nil) => (vm => vm) case (Succ(n), Cons(a)(vn)) => val concatVn = concat(vn) vm => Cons(a)(concatVn(vm)) } 

Testing:

 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))))) 

Let me show you another example of how theorems are proved in ProvingGround. We prove that 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) ) 

A circle cannot be defined as an ordinary inductive type through (...) |: (...) =:: ... (indeed, the loop constructor returns not a value of the Circle type, as it would be for an ordinary inductive type). Therefore, recursion with induction has to be determined manually:

 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) ) 

with two axioms comp_base and 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 ) 

A few words on how to run the code on ProvingGround. There are 3 ways.

1. The first and recommended - from the console (loaded Ammonite REPL ) using the command
   sbt mantle / test: run (from the root of the ProvingGround project after cloning the repository github.com/siddhartha-gadgil/ProvingGround.git , in the case of the Ammonite REPL launch error, create an empty ProvingGround/mantle/target/web/classes/test ) directory.
   
   
2. The second is using the sbt server/run command and then opening http: // localhost: 8080 in the browser.
   
   
3. The third is from the IDE. In IntelliJ Idea 2017.1.3, the project may be imported after modifying build.sbt, but the code may not run. The solution is to import into the Idea not the entire project, but only the ProvingGround/core subproject. To do this, put a new build.sbt here: ProvingGround/core/build.sbt .
   
   List of imports:
   
   

    import provingground._ import HoTT._ import TLImplicits._ import shapeless._ //import ammonite.ops._ import FansiShow._ 

If anyone is interested in this topic (type theory, homotopy type theory, dependent types, type-level calculations, automatic proof of theorems), welcome to my course . He is introductory. According to HoTT, it’s rather not even an introduction, but an introduction to the introduction, but in other areas, I think, it falls short of the level of an introduction. Thanks for attention.