2012/07/27 04:46:12
While Scala 2.10 is being prepared, I'd like to think what Scala 3 might look like.

Part Ø: Aliases for context bounds

As you probably know, Scala posesses both a trait >Ordered and a typeclass Ordering[_]. The typeclass is the right way to impose an order, the trait that demands comparison operator inside objects is a wrong way that will be deprecated someday. However, it's easier to write sort(xs: List[Ordered]) than sort[T: Ordering](xs: List[T]). For many people, second notation is a burden. We can take best of both worlds if we allow Ordered to be alias for context bound. Bound aliases should be declared as sealed abstract types for they can not be instantiated or extended, but can be used in any context abstact type can.*
Now here's the example of syntax I'd propose:
sealed abstract type Ordered = T forSome Ordering[T]

Such alias now works so that sort(xs: List[Ordered]) gets desugared to sort[T: Ordering](xs: List[T]).

The notation on the left hand side (sealed abstract type) is new, while the notation on the right hand side becomes valid if we treat generics as a syntax sugar for abstract type members in lieu of SIP 18, see this discussion. It's almost equivalent to “o.T forSome {val o: Ordering}”.

This syntactic sugar is not compatible with present Scala for context bounds are allowed not in all cases where usual lower bounds are. In the part II I will strongly argue for allowance of context bounds everywhere in lieu of “Context Bounds for Abstract Type Members” (https://groups.google.com/forum/?fromgroups#!topic/scala-internals/eThZIT6y5pM).

The presented syntactic sugar simplifies typeclass based programming to a great extent and is vitally necessary for thing's I'm going to talk in the next section.

Part I: Make values behaviorless!

The central notion of object oriented programming are the objects: these are typically mutable things with individual identity and lifecycle. Objects (except static ones) are created with "new" operator and destroyed at some point later. They can be active (actors) or passive (entities), their state is typically encapsulated ("hidden") and can be accessed directly only by their member methods. Scala (already as of 2.10) has achieved the perfection in OOP, everything I'm aware concerning OOP can be done in Scala in proper and elegant way. Scala has both a proper and simple internal formalism and a multitude applied techniques built atop of it: companion objects (proper replacement for static methods), generics (including proper variance handling), inheritance (including proper multiple inheritance), mix-in composition, cake pattern, direct support of actors, etc.

What Scala 2.xx neglects are the values. Values are immutable behaviorless things like for example numbers, they don't have any lifecycle, they're never created or destroyed, they just are. Being immutable and behaviorless means they cannot have (nonstatic) methods or state. (Recall that static methods belong to companion objects.)
Currently, values are emulated by immutable objects, which is not entirely correct. In Scala 2.xx the instruction "2 + 3" means "2.add(3)", which is "dear number 2, please add 3 to yourself", nonsence isn't it? The addition, an entirely symmetrical operation, is broken: it is dispatched to the first operand and is though polymorphic only in the first operand and generic only in the second one. If has complete access to the implementation details of the first operand, but not the second one. This is a very serious leaky abstraction, the only remaining Java'esque crutch of Scala I'm aware of. It's the sequel of one of the most vicious flaws of Java: static methods. In Scala, there are no static methods any more, they were superseded by companion objects. But the methods that ought to belong to the companion objects (like add(a, b)) are still often placed into the class. Note that it's not the problem of the language itself but is mainly the problem of standard library. With syntactic sugar form the part Ø and little changes in operator handling, it can be solved completely, without any changes to the language core.

A value like 2 cannot have a method like "add", the additivity is not a property of a single number, but of the class of the numbers. Numbers can be added owing to the fact that they belong to a type with a certain structure (additive one), and the instruction "2 + 3" should read "Int.add(2, 3)", where Int is the companion object of Int type, the object which actually has methods for manipulating the Ints. Generally, for value types expressions like a OP b should be treated as (companionObjectFor(a) merge companionObjectFor(b)).OP(a, b) with obvious default definition of "merge".

Simplest value types are enumeations (type MonoColor = White | Black) and parametized enumerations (case classes). If you allow for recursive parametrized enumerations, you'll be able to provide low-level models for any computationally viable value type. Functional languages from Lisp family (including Clojure) and Haskell familiy (including Agda) work with such low level datatypes (concrete datatypes). They don't allow to abstract out (encapsulate) the implementation details and define an abstracted datatype like Int (of integer numbers), which are of course internally based on low-level implementation, but forget about it and provide a higher-level interface which is then the only way to interact with them.

In Scala (in the tradition of ML family languages) you have instruments for encapsulation. Here's the code:
implicit object Int extends Ring {
  type T = // low level implementation
  def add(a: T, b: T): M = // low level implementation
  ...
}
type Int = Int.T

After such a definition, all implementation details are hidden in the companion object Int, while the type Int has no other properties than being manipulatable by methods from the object Int. In the next section we'll explain that in (a bit extended) Scala we can describe all value types from mathematics correctly, without leaky abstractions or simplifications which are typical fetters of programming ecosystems.

Scala would become a much better language if numbers and immutable collections would be made pure values, so that "2 + 3" would mean "Int.add(2, 3)" and "list map func" would mean List[T].map(func)(list). The superclasses of values such as Numeric and Traversable[T] would be no traits but typeclass based interfaces:
sealed abstract type Numeric = N forSome Arithmetic[N]
sealed abstract type Enumerable[T] = C forSome Enumerator[T][C]

Part II: What type system should Scala 3 be based on

Scala 3 certainly has to be based upon DOT+DMT.
Dependent Object Types is a nominal type system, which subjects are essentially dependent tuples which can contain abstract type members besides normal members. Dependent Method Types is its extension providing dependent products in addition to dependent sums (tuples, mentioned above). Together they provide a complete and very nice propositions-as-types encoding for first-order logic, which relates it to constructive type theories.

DOT is an open-world theory, it assumes existence of types which are not defined (or definable) within the system, but one can still work with objects of these types when the come with modules of operations working on them. Even though these operations are not and cannot be defined within DOT, they still can be used in it: one can compose them with other operations of compatible signatures. A concrete example would be the type of Reals, which are in general not representable in finite amount of computer memory and thus not definable within any constructive type theory, but assuming such type "exists in the outer world" we can write down programs working with them and reason about this programs even though we're not able to execute them. What's the use of that? — Well, after having defined a program for Reals we can translate it into a program manipulating Doubles (floating point numbers) and analyse if the latter is a correct approximation of the former.

DOT is not yet a complete calculus, the indisputable core is very weak and not sufficient to carry out complex proofs or computations. In this essay I will argue that we should stick to the core without extending it to the full strength of Fω with unrestricted recursion! There should be a weak core and pluggable completions producing dialects for reflecting different topoi (mathematical setups) to work in. The core is flexible enough to be adapted for arbitrary topoi to work in, from the classical ZFC set theory to Calculus of Constructions to Homotopic Type Theory. It's of course also fit for the legacy Scala topos, constituted by computations which can be carried out on an idealized JVM.

Part III: Brief explanation what theories and models are and exposition of the syntax we need to describe theories comfortably

Bourbaki said, mathematics studies structures. In modern language one could rather say, a mathematics studies theories and their models. Back in Bourbaki's days, only set-theoretic models were studied for set-theoretic representation was considered ‘concrete’. Today people study models in many different topoi. Mainstream mathematics still works preferrably in the realm of ZFC set theory, but foundations people and computer scientists often prefer constructive type theories, which are ‘concrete’ in much stronger sense than the ZFC set theory.

What's a theory anyway? A theory consists of a signature and a couple of properties it must conform to. Signature consists of a couple of abstract type members and members of specified types. Here's a signature of a semigroup (not quite complete):
trait Semigroup {
  type G
  def compose(a: G, b: G): G
}

Predicates can be modeled either as types or like operations returning Boolean, the latter is easier to understand for programmers and is also the topos-theoretic way. Here's a signature for equality theory:
trait Eq {
  type T
  def eq(a: T, b: T): Boolean
}

We can also incorporate properties. Say, eq must be built so, that eq(x, x) is true for any x. So, we might demand the proof of that fact in the signature. For boolean expressions, there's an inner type .Evidence, which is the type of proofs that the expression is true. So, that's how we encode it:
trait Eq {
  type T
  def eq(a: T, b: T): Boolean
  def reflexivity(x: T): eq(x, x).Evidence
}
(Please note that we're not using actual Scala 2.x code but wild fantasy on how Scala 3 might work! In Scala 2.x the type eq(x, x).Evidence won't work because eq(x, x) is not a stable identifier. We still can mock such types with macros in Scala 2.x but this doesn't seem to be kosher.)

Path-dependent types of Scala DOT formalism and dependent method types are both the essential ingridients allowing to do so. Let's also encode the transitivity:
trait Eq {
  type T
  def eq(a: T, b: T): Boolean
  def reflexivity(x: T): eq(x, x).Evidence
  def symmetry(x: T, y: T)(a: eq(x, y).Evidence): eq(y, x).Evidence
  def transitivity(x: T, y: T, z:T)(a: eq(x, y).Evidence, b: eq(y, z).Evidence): eq(x, z).Evidence
}

А model for a given signature is a named tuple assigning concrete types, concrete implementations of operations and concrete proofs demanded by signature. Concrete means, they are explicitly constructed in the topos (or a weaker realm) inside of which we model our structure. Trait (signature) is a type for corresponding models.

The semigroup theory is a theory with equality, here's its complete signature:
trait SemiGroup {
  type G
  def G: Eq[T = G]
  def compose(a: G, b: G): G
  def associativity(a: G, b: G, c: G):
    G.eq(
      compose(a, compose(b, c)),
      compose(compose(a, b), c)
    ).Evidence
}
(It's not bad we used the same letter to denote a type and a constant for they can be always differentiated from context. The expression Eq[T = G] "named generic" is shorthand for Eq {type T = G}.)

Now let me introduce some syntactic sugar that saves lots of space and is also quite enlightening. In most cases, a theory looks like a certain type endowed with a certain structure, so one of the member types has a distinct role. There's a special syntactic sugar for it:
trait Eq[T] {
  def eq(a: T, b: T): Boolean
  def reflexivity(x: T): eq(x, x).Evidence
  def transitivity(x: T, y: T, z:T)(a: eq(x, y).Evidence, b: eq(y, z).Evidence): eq(x, z).Evidence
}
(We'll in general treat generics as a syntax sugar for abstract type members in lieu of SIP 18, see this discussion.)

Such signatures, can be treated as so called typeclasses, ‘types for types’. The construction
 type G
 def G: Eq[G] 
is now shorthanded to type G: Eq. We can now write
trait SemiGroup {
  type G: Eq
  ...
}
or
trait SemiGroup[G: Eq] {
  ...
}

For the common case you want to import the members of one model into the other there is another syntactic sugar called inheritance:
trait Monoid[M] extends SemiGroup[M] {
  def unit: M
  def leftCancelativeness(x: M): M.eq(unit, compose(unit, x)).Evidence
  def rightCancelativeness(x: M): M.eq(unit, compose(x, unit)).Evidence
}
type VectorSpace[V] extends AbelianGroup[V] = {
  type F: Field
  def action(scalar: F, vector: V): V
  ..
}

How to write proofs
Say you want to prove that a monoid has only one unit, i.e. every element of monoid havind the left or right cancellation property is equal to the unit. In other words, we want to define a procedure which being “given an element unit2 with left cancellation property” produces an “evidence that unit2 is the same as unit”:
def lemma1[M: Monoid](unit2: M)(leftCanc2: (x: M) => M.eq(unit2, M.compose(unit2, x)).Evidence) = {
  // apply left cancellation property of unit2 to unit and vice verse
  val p1: M.eq(unit2, M.compose(unit2, M.unit)).Evidence = leftCanc2(M.unit)
  val p2: M.eq(M.unit, M.compose(unit2, M.unit)).Evidence = M.rightCancellation(unit2)
  // now we just have to simplify “unit2 = something = unit” to “unit2 = unit”
  val p3: M.eq(M.compose(unit2, M.unit), M.unit).Evidence =
      M.symmetry(unit, M.compose(unit2, M.unit))(p2)
  val p4: M.eq(unit2, M.unit).Evidence =
      M.transitivity(unit2, M.compose(unit2, M.unit), M.unit)(p2, p3)
  p4
}
The used dependent function type is a shortcut:
(x: M) => eq(unit, compose(unit, x).Evidence) ≡ {
  def apply(x: M): eq(unit, compose(unit, x).Evidence
}

The notation Type[_] is used not only for typeclasses, these are generally ‘types parametrized by other types’. Due to availability of subtyping constrants on abstract type members, in DOT we can demand abstract type members (or type parameters) of traits to be not just types, but types parametrized by other types, so called higher kinded types.

Beautiful example is provided by semicategories and categories which are "typed" versions of semigroups and monoids. You can always think of a semigroup as consisting of functions with their usual composition which is naturally associative. These must be functions type T => T for some fixed type T (say, real numbers) so that their composition is always defined. Semicategory is the generalization for the case we have many types and only functions with matching source and target types can be composed. Monoid is semigroup with unit, category is a semicategory with units. The signatures of semicategory and category repeat the ones of semigroup and monoid in all respects except that in first ones we had one type T of the semigroup/monoid elements, whereas in second ones we'll have parametrized (by source and target) families Arr[_,_] of element types:
trait SemiCategory[Arr[_,_] : Eq] {
  def compose[A, B, C](a: Arr[A, B], b: Arr[B, C]): Arr[A, C]
  def associativity[A, B, C, D](a: Arr[A, B], b: Arr[B, C], c: Arr[C, D]):
    Arr[A, D].eq(
      compose(a, compose(b, c)),
      compose(compose(a, b), c)
    ).Evidence
}
trait Category[Arr[_,_] : Eq] extends SemiCategory[Arr[_,_]] {
  def id[O]: Arr[O, O]
  def leftCancelativeness[O](x: M): Arr[O,O].eq(id[O], compose(id[O], x)).Evidence
  def rightCancelativeness[O](x: M): Arr[O,O].eq(id[O], compose(x, id[O])).Evidence
}
(In Scala 2.x, the notation T[_] presupposes that the polymorphic type T should accept any types as arguments and in general, when bounds of type-parameter in a polymorphic definition are not specified, absence of bounds is presupposed. We suggest that in Scala 3 when no bounds for type parameters are specified, the most broad bounds allowed by the rest of the signature should be taken. It spares vast amounts of unnecessary writing. In particular, we want the definitions above to be applicable to types of functions on restricted or extended type universes, e.g. Function[A &;lt;: Collection, B <: Collection] (function between collection types) or Function[A: Ord, B: Ord] (functions between types endowed with order).)

The last thing we want to explore, is how to write signatures of theories which make use of ‘powerset’ and ‘subsets’ (powerobjects and subobjects in general setting, where we don't restrict us to set-theoretic topoi). Well, in general topoi, these are constructed using the _ => _ type (type of maps from one type to the other) and Boolean type (which is called subobject classifier in general setting). First note, that ‘subsets’ S of A are classified by maps isMember: A => Boolean.
So, the type of subobjects of T can be defined as
trait Restriction[T]  {
  def isMember(x: T): Boolean
  type Element = T with {self =>
    membership: isMember(self).Evidence
  }
}
(We can explicitly define the type for elements of the restriction as a dependent pair)

Once you have a restriction r: Restriction[S], you can define functions from elements of this restriction:
val even = Restriction[Nat](isMember = (_ % 2 == 0)) 
// Shorthand for new Restriction[Nat] { def isMember(x: Nat) = ... }
def bisect(x: even.Element): Nat = ...

We can also easiliy define structures like topology:
trait TopSpace[S]  {
  def topology: Restriction[Restriction[S]]
  ...
}

In DOT there is a subtyping relation which allows to use expressions of one type in the context where another type is expected in cases this is entirely safe and transperent. It solves the following two issues:
– Functions A => B to be applicable to terms of types which are restrictions of A;
– Stronger structures such as monoids to be accepted in context where a weaker structure (such as a semigroup) is required.

DOT uses a cumbersome mixture of nominal and structural subtyping which we I don't want to describe here completely, but I just want to underline that the mentioned features are solved by DOT perfectly: restriction types (as defined above) are subtypes of the types they restrict, stronger signatures are subtypes of weaker ones. Subtyping relation enables specifying lower and upper bounds for abstract type members of traits, which is precisely the mechanism that makes nominal induction, higher kinded types and lots of other valuable things possible.

Subtyping relation for types internal to DOT (i.e. traits) is even a complete one, traits build a lattice, their least upper bounds and greatest lower bounds are always well defined, which can be used to demand a type to conform to two signatures in a coherent way:
radixSort[T: Ord ∨ Weighted](xs: Collection[T])

The complicated issue is the subtyping for abstracted value types. We want all containers (List, Tree, etc) to be subtypes of Collection and Nat (natural numbers) to be subtype of Int. Iff abstracted type A (say, Nat or List) has a unique natural embedding into B (say, Int or Collection), we want that A <: B. So far I have no concrete idea how to implement it on the type system level.
* * *

This was an exposition of the trait definition sublanguage of Scala. When you're not using path-dependent types, like, say .Evidence or .Element, the language has no term-level constructions, we only define member names and their types in a straightforward ways, interpretable in any category with finite products (or more generally, any circuitry) with all external types we use, like, say, Boolean, provided. The trait itself (as a type) will lay inside the category/circuitry iff the trait contains only types and constants or the category/circuitry is a (cartesian) closed one. Otherwise it lays in the enclosing topos.

When path-dependent types are used, suddenly the term-level language arises (see the expressions like compose(x, unit) above). They can contain creation of modules and member extraction (harmless things interpretable in all circuitries), but also application and (dependent) abstraction, which are interpretable only in (locally) closed categories/circuitries.

As opposed to Per Martin-Löf style type systems, where types-level and term-level are rigidly unified, DOT uses managed lifts between term-level and type/judgement-level:
Term-level → type-level: path-dependent types.
Type-level → term-level: typeclass-bound polymorphism.
By enhancing or restricting the richness of terms allowed in trait signatures (i.e. by working in more or less powerful topoi), one can precisely control the tradeoff between expressiveness and manageability.

Part IV: Implicits: Enabling practical use of proofs

In Scala, you can mark some arguments of your functions with the annotation named @implicit. It means, the compiler would try to guess the correct object to pass as the argument from the context or would rise a compile time error if it cannot guess or has multiple variants. The annotation does not prevent passing the argument explicitely if you know better.

There are operations which can be performed only if some fact is known in the compile time. For example, you can deterministically extract an element from an unordered collection iff it's size is one. Here's the signature of such an operation:
def the[T](x: Collection[T])(@implicit uniqueness: (size(x) == 1).Evidence): T

Here, T in brackets means our operation is polymorphic in the sense you can put any type instead of T and get a specialized version and then use it. Then the operation takes a collection and a proof that it contains one element, and then returns the element back. If the compiler can assure in compile time that the first argument has size 1, it would supply the evidence automatically, that's how the @implicit annotation works; in 99% you shouldn't care proving anything yourself, it'll take care. In the 1% cases you know how to show this fact in compile time although compiler wouldn't guess, you can do it by hand. (The better strategy is to enhance the compiler by a plugin which handles your situation automatically.)

One very interesting usage of the analogon of the ‘the’ operation, is the extractor of universal objects. If you have a typeclass (say, PeanoArithmetic[_]) which is known to be constructively categorical (to have one and only one minimal model up to uniquee isomorphism) (in a particular category), you can extract the model, which is then known as an universal object (say, Nat, the type of natural numbers):
implict val Nat = zfc.universal[Semiring]
implict val Int = zfc.universal[Ring]
// Also true:
implict val Nat = zfc.universal[PeanoArithmetic]
    with InductiveAddition, InductiveMultiplication
Two latter traits define + and * via succ of PA

For some operations, knowing additional facts just speed them up. Say, you want to reduce a list by a binary operation. It always takes not more than n executions of the operation, but if the operation is associative, on a machine with data parallelizm, you can perform the reduction in O(log n) operation, which is an exponential speedup! To use this advantage, write two different versions of reduce, and an implicit converter
def reduce[T](op: BinOp[T]): T
def reduce[T](op: AssocBinOp[T]): T
implicit def toAssocBinOp[T](op: BinOp[T])(@implicit associativity:
  ((a: T, b: T, c: T) => op(op(a, b), c) == op(a, op(b, c))).Evidence
) = AssocBinOp(op, associativity)

There is a parallel annotation @inferred for abstract trait members that means they should be filled automatically every time the trait instance is created, so they become @implicit arguments of the constructor. Whereas context bounds of polymorphic functions desugar to @implicit arguments, context bounds in traits desugar to @inferred members.

When you define a model of a monoid, you'd perhaps prefer to specify only the definition for composition and let the compiler try to find the proofs for associativity and so on. So, in the signatures of the theories, the proofs should be marked @inferred as well:
trait Monoid[M] extends SemiGroup[M] {
  def unit: M
  @inferred def leftCancelativeness(x: M): eq(unit, compose(unit, x)).Evidence
  @inferred def rightCancelativeness(x: M): eq(unit, compose(x, unit)).Evidence
}


Other usages of implicits
Implicits can be also used for enforcing compile time constraints. A polymorphic operation could take a PerformanceConstraint, by default an empty one:
seek(where: Location)(@implicit in: PerformanceConstraint)
But once you want to ensure, the correct algorithm would be taken, just do
seek(somewhere)(PerformanceConstraint("O(1)"))

Implicits can be also used to set the preffered method for routines, which have multiple implementations (like sorting) and to tell optimisation macros which strategy to use. The main use of implicits is in typeclass-based polymorphism, see below.

Today there are three mechanisms for generation of objects the compiler would pass around as implicit arguments:
– You can specify so called implicit values, they'd be found by their types
– You can specify implicit conversions, which are used by the compiler as derivation strategies for implicit objects
– You can define so called implicit macros, which are essentially just programms generating implicits, and could be built as mighty as you wish. The automatic proof seekers should be implemented via implicit macros.

It would be very practical to implement cascading implicit policies, which would provide a very flexible and transparent method for specifying implicit resolution policy. These should be built very much like css for html:
com.miriamlaurel.cascade.test4 {
  FunctionInlining = Moderate
  SortingMethod = scala.util.Sorting.quickSort
  Ord[String] = I18n.AlphabeticOrders.Swedish

  TestObj#cacheCriticalMethod {
    SortingMethod = scala.util.Sorting.insertionSort
    FunctionInlining = Agressive
    LoopFlattening = Agressive
    Synchronization = Optimistic
  }

  TestObj#wellParallelizableMethod {
    ImplicitParallelization = Moderate
    SortingMethod = scala.util.Sorting.mergeSort
    ReductionStrategy = Optimistic
    Ord[String] = I18n.AlphabeticOrders.Default
  }
}
By using explicit arguments, implicits (including the ones from cascading implicit policies of course) can be overriden where necessary.


In Scala 2.xx, every function is allowed to have only one implicit argument list, which is the last one. It's not allowed to do something like
def f(implicit a: Sometype)(b: a.T)
which can be quite burdensome. For this reason we want to provide @implicit macro annotation which is more flexible in this respect and is allowed to be used on arguments in random order. In order to specify the values for implicit arguments on the call site you'll have named arguments like this
// The definition
def f(@implicit implArg1: Sometype)(b: a.T, c: Int)
// Normal usage
f(arg1, 4)
// Explicitly specify everything
f(arg1, 4)(implArg1 = explictValue)


Part V: Typeclass-based polymorphism and open world setting

As we already mentioned, DOT doesn't assume, all types are defined inside of DOT, some might come externally (open world). Now consider a polymorphic function
def foo[T](x: T, y: T)
What can be done to the arguments in the body of the function? Absolutely nothing! Because, there is nothing you can do to values of unknown type, not even check their equality. Even though all types that can be defined within Scala automatically come with equality, we do not assume that all types have equality. The open world setting for typed systems reads “Inconstructibility of type does not imply its nonexistance”, which is closely related to open world assumption of ontology systems “Inability to derive a fact does not imply the opposite”. In practice, the types that are nonconstructible represent codata, such as possibly infinite sequences or (true) real numbers. (Of course, you can generate some infinite sequences deterministically and construct lots of real numbers, but constructible sequences/reals form an infinitely small fraction of all possible ones.) Constructible are only the interfaces (typeclasses) for codata types, Seq[Int] being an example.

To be able to do something, you must restrict, you must assume that T is endowed with some structure. For instance, like this:
def foo[T: Eq](x: T, y: T)
This is a shorthand for
def foo[T](x: T, y: T)(@implicit T: Eq[T])
So, the function takes an additional hidden argument: the model for the theory Eq[T], i.e. a tuple, where the operation eq(x: T, y: T) that checkes the equality, is defined. It's no problem that I have used the same name for the type and for the associated model, they can always be differentiated from the context.

No we can write something into the body of foo, for instance
def foo[T: Eq](x: T, y: T) = T.eq(x, y)
One of the main strengths of Scala is the presence of encaplulation, i.e. we can abstract out the implementation details of a certain type and forbid any functions to interact with instances of the type in any other way through the defined interface (signature).
implicit val m: Monoid = new Monoid {
  type M = (Nat, Int)
  def compose(a: M, b: M): M = ???
  // Implementation details, which are aware that M = (Nat, Int)
}
type M = m.M
// Implementation details of M are now hidden, you
// cannot find out that M = (Nat, Int) in the outer scope.*
// The only thing you know about it is that M : Monoid,
// since there is a defined implicit model Monoid[M].
// (* Runtime reflection not considered for it's
// a low level non-typesafe technique.)

There is a plenty of real-life examples for type-class bound polymorphism
def sort[T: Ord](xs: Collection[T]): List[T]

... and very few with unbound polymorphism:
def first[T](xs: List[T]): T
def the[T](x: Collection[T])(@implicit uniqueness: (size(x) == 1).Evidence): T
Note that in Scala 2.xx context bounds implicit arguments are always last ones, so foo[T: C](args) always desugar to foo[T](args)(implicit T: C[T]). In our proposal implicit arguments can appear on any position, so we'll desugar it to foo[T](@implicit T: C[T])(args) (for the sake of compatibility to other functional languages) and fall back to foo[T](args)(@implicit T: C[T]) only if the type C depends on args as in def f[T: c.TypeTag](c: Context)(t: c.Expr[T]).

If we restrict our world to types types from some defined topos, say [T: zfc.Set] or [T: agda.Set], we immedeately pass to realms of corresponding topoi. Just consider how the signatures look after erasure in such case:
// Originally
last[T: agda.Set](xs: agda.List[T]): T
// Resolve implicits, perform erasure:
(T: agda.Set) => agda.list(T).Type => T.Type
// Or in agda notation
{T: Set} -> List T -> T


The difference is, of course, that topoi like agda.Set can be equipped with operational semantics and used for computations, whereas, set theory can be essentially used only for reasoning and making proofs, because most of its operations operations are not constructive (either non-computable, or non-deterministic such as taking an arbitrary element from a set of size > 1).

Legacy Scala works in a topos jvm.Type, i.e. not in an open world, but in a world where every type is either a class, a primitive JVM type or an array of jvm.Type elements and the information which jvm.Type corresponds to a given type T is available on term-level (i.e. in runtime) for all terms. So, formally every time you have a function with an argument of a non-final type, you also implicitly pass the jvm.Type-information on the exact type of the argument:
// What you write in legacy Scala:
def first[T](xs: List[T])
// formally:
def first[T](xs: List[T])(@implicit xsRuntimeType: jvm.Type[List[T]])

By formally I mean that the implicit argument xsRuntimeType is not really passed, but the information in contains is available (say, through the instanceof operator) in the body of the callee out of thin air. In order to reflect this fact on the formal level we do so as if it were originally returned together with each created object by the new operator and then passed from the caller to callee on each call.

jvm.Type of List[T] would not contain any information on T, but from Scala 2.10 you can use Scala TypeTags, that carry such kind of information, so from 2.10 we'll be working in an another topos, a topos where it's assumed instead that every type implicitly caries its typetag:
def first[T](xs: List[T]) ≡ first[T](xs: List[T])(@implicit xsRuntimeType: TypeTag[List[T]]).

How does the agda-in-scala encoding work
In Per Martin-Löf style typesystems types can appear both on as types and as terms. In Scala we have to differentiate. We will represent the expression level manifestations of agda types as values of the type agda.Set, and whenever t: agda.Set has to be used on the type side, perform the lifting t.Type. In the agda signature {T: Set} -> T, the symbol T appears once as a term and once as a type, so its Scala representation would be (T: agda.Set) => T.Type.

So, the trait Set carries information about how an Agda type is built, it can be a finite enumeration, a (dependent) tuple type, a (dependent) function type etc. Additionally it has one type member called Type for lifting between term and type levels. For convinience we make it to a typeclass:
trait Set[Type] {
   ???
}

We also provide some common inductive datatype families:
list(t: Set): Set = ???
pair(a: Set, b: Set): Set = ???

For convinience we also provide aliases:
type List[T: Set] = list(T).Type
type Pair[A: Set, B: Set] = pair(A, B).Type

Now you're ready to analyse
last[T: agda.Set](xs: agda.List[T]): T
// Desugar context bounds:
last[T](t: agda.Set)(xs: agda.List[T]): T
// Desugar type aliases
last[T](t: agda.Set)(xs: agda.list(t).Type): T
// Pre-erasure type normalization
last[T](t: agda.Set)(xs: agda.list(t).Type): t.Type
// Perform erasure
(t: agda.Set) => agda.list(t).Type => t.Type
// Compare with Agda:
{T: Set} -> List T -> T



Part VI: Frontiers of Modularity: Defining DSLs

Scala 2.10 is already a very modular and extendable system, where the compiler can be naturally extended with help of macros mechanism. 2.10 does not readily provide macro types, and also the process of type checking cannot be yet extended, but there are plans to include them in future. As I already mentioned, in my vision, Scala 3 should consist of a weak core (essential DOT) and a multitude of pluggable and partially intermixable extensions (DSLs) which in particluar can be used to extend DOT to include other type systems (or, more generally, type- and effect systems).
DSL descriptions would contain:
1) Primitives and a DSL for their comfortable usage
2) Pre-erasure type normalization procedure
3) Type constructors and type checking rules concerning new primitives
4) Optionally, extension rules for type inference, equiality checking, term normalisation and unification.
With a little help of macros and circuitry formalism (AKA generalized arrow formalism from the article "Multi-Level Languages are Generalized Arrows") which is a vast generalization of Scala Virtualized, this can be done very elegantly. You'll just have to define the circuitries/categories/topoi for DSLs you want and import them with normal import keyword to enable/switch to the given DSL.

As a result, we can make DSLs for total programming (no possibility of infinite loops and unhandled exceptions), DSLs with typed effects, DSLs for secure real time programming, DSLs for safe numeric calculations, DSLs for massively parallelized information processing, DSLs for quantum computing, and, last but not least, DSLs for mathematics that turn Scala into a novel theorem checker/proof assistaint with unprecedented flexibility of notation.
0 посетителей, 22 комментария, 2 ссылки, за 24 часа