Scala Representations

Scala objects are integrated with HoTT by using wrappers, combinators and implicit based convenience methods. In this note we look at the basic representations. The main power of this is to provide automatically (through implicits) types and scala bindings for functions from the basic ones.

A more advanced form of Scala representations also makes symbolic algebra simplifications. The basic form should be used, for example, for group presentations, where simplifications are not expected.



In [1]:

    
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
import provingground._ , interface._, HoTT._









    Out[1]:





import $ivy.$                                       

import provingground._ , interface._, HoTT._



In [2]:

    
import provingground._
import HoTT._, scalahott._
import ScalaRep._









    Out[2]:





import provingground._

import HoTT._, scalahott._

import ScalaRep._

We consider the type of Natural numbers formed from Integers. This is defined in ScalaRep as:

case object NatInt extends ScalaTyp[Int]

Warning: This is an unsafe type, as Integers can overflow, and there is no checking for positivity.



In [3]:

    
NatInt









    Out[3]:





res2: NatInt.type = NatInt

Conversion using the term method

The term method converts a scala object, with scala type T say, into a Term, provided there is an implicit representation with scala type T.



In [4]:

    
import NatInt.rep
1.term









    Out[4]:





import NatInt.rep

res3_1: RepTerm[Int] = RepSymbObj(ScalaSymbol(1), NatInt)

Functions to FuncTerms

Given the representation of Int, there are combinators that give representations of, for instance Int => Int => Int. Note also that the type of the resulting term is a type parameter of the scala representations, so we get a refined compile time type



In [5]:

    
val sum = ((n: Int) => (m: Int) => n + m).term









    Out[5]:





sum: Func[RepTerm[Int], Func[RepTerm[Int], RepTerm[Int]]] = ExtendedFunction(
  ammonite.$sess.cmd4$Helper$$Lambda$2363/1189219296@57a4cd68,
  SimpleRep(NatInt),
  FuncRep(SimpleRep(NatInt), SimpleRep(NatInt))
)



In [6]:

    
sum(1.term)(2.term)









    Out[6]:





res5: RepTerm[Int] = RepSymbObj(ScalaSymbol(3), NatInt)



In [7]:

    
val n = "n" :: NatInt
sum(n)(2.term)









    Out[7]:





n: RepTerm[Int] = RepSymbObj(Name("n"), NatInt)
res6_1: RepTerm[Int] = RepSymbObj(
  ApplnSym(
    SymbolicFunc(
      ApplnSym(
        ExtendedFunction(
          ammonite.$sess.cmd4$Helper$$Lambda$2363/1189219296@57a4cd68,
          SimpleRep(NatInt),
          FuncRep(SimpleRep(NatInt), SimpleRep(NatInt))
        ),
        RepSymbObj(Name("n"), NatInt)
      ),
      NatInt,
      NatInt
    ),
    RepSymbObj(ScalaSymbol(2), NatInt)
  ),
  NatInt
)



In [8]:

    
val s = lmbda(n)(sum(n)(2.term))









    Out[8]:





s: Func[RepTerm[Int], RepTerm[Int]] = LambdaFixed(
  RepSymbObj(n, NatInt),
  RepSymbObj(
    ApplnSym(
      SymbolicFunc(
        ApplnSym(
          ExtendedFunction(
            ammonite.$sess.cmd4$Helper$$Lambda$2363/1189219296@57a4cd68,
            SimpleRep(NatInt),
            FuncRep(SimpleRep(NatInt), SimpleRep(NatInt))
          ),
          RepSymbObj(n, NatInt)
        ),
        NatInt,
        NatInt
      ),
      RepSymbObj(ScalaSymbol(2), NatInt)
    ),
    NatInt
  )
)



In [9]:

    
s(3.term)









    Out[9]:





res8: RepTerm[Int] = RepSymbObj(ScalaSymbol(5), NatInt)

We will also define the product



In [10]:

    
val prod = ((n : Int) => (m: Int) => n * m).term









    Out[10]:





prod: Func[RepTerm[Int], Func[RepTerm[Int], RepTerm[Int]]] = ExtendedFunction(
  ammonite.$sess.cmd9$Helper$$Lambda$2430/434006696@6c9e4bf0,
  SimpleRep(NatInt),
  FuncRep(SimpleRep(NatInt), SimpleRep(NatInt))
)



In [11]:

    
prod(2.term)(4.term)









    Out[11]:





res10: RepTerm[Int] = RepSymbObj(ScalaSymbol(8), NatInt)



In [ ]: