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 [ ]: