The far side of Scala

[Ben Hutchison]

It finally happened. In recent days, I switched for the first time
from discovering what I _can_ do with Scala to discovering what I
_cannot_.

Ive been thinking about situations in which I know much more about
what code does or should do, at compile-time, than I can express in
Scala's type system.

I present here some example use cases in pseudo-Scala:


//The value returned by this method can be viewed as a subtype of Int,
being a Int between 0 inclusive and bound, exclusive.
val index = random.nextInt(bound: Int): Int{0 <= value < bound}

val smallerArray: Array[Int]{length == bound - 1} = new Array[Int](bound - 1)
val largerArray: Array[Int]{length == bound} = Array[Int](bound)

val elem1 = smallerArray(index)  //compile warning or error
val elem2 = largerArray(index)  //no bounds checking required

abstract class Matrix[Num](val rowCount:Int, val columnCount:Int,
values:Seq[Num]{length >= self.size})  { self =>

  def multiply(other:Matrix): ResultMatrix match {
    //this pattern match determines the method return type!
    case rowCount == other.columnCount => SquareMatrix
    case rowCount < other.columnCount => FatMatrix
    case rowCount > other.columnCount => SkinnyMatrix } = {
      new ResultMatrix(rowCount, columnCount, for (row <- rows; column
<- other.columns) yield row.dot(column))
    }

  def rows:Seq[Seq[Num]] = {...}
  def columns:Seq[Seq[Num]] = {...}
  def size = rowCount * columnCount
}
class SquareMatrix  extends Matrix{columnCount == rowCount}  {}
class FatMatrix  extends Matrix{columnCount >= rowCount}  {}
class SkinnyMatrix  extends Matrix{columnCount <= rowCount}  {}


My knowledge of formal type theory is basic, but I think what is
needed to express the above relations are Dependent Types (types that
depend upon values). A couple of hours internet research suggests that
Dependent Types are a young field with comparatively unexplored
territory.

When I consider how the above pseudo-Scala would execute, I notice that:

1. Tagging objects with a type based on their value works much better
with immutability than mutability, so such techniques might compliment
an Effect System that controlled or tracked mutation.

2. There is a glaring chicken-and-egg problem. The value-dependent
constraints can be threaded through any quantity of dependently-typed
code, but it all has to begin with an entry point from the outside
world, where the first values originate. For example, we might read
the values of a Matrix from a file, and thus have no prior idea about
its row or column sizes.

3. From the implications of point 2, a picture emerges of code that
can be evaluated /at the earliest possible time that its dependencies
are available/. Sometimes this will be at compile time, sometimes once
during runtime initialization, and other times repeatedly during
execution. Compile-time Types and Runtime Values become inter-woven.
At the limit, types describe programmer intent so thoroughly that
typechecking and executing a program converge.


My relative ignorance of type-theory and compiler design means I
probably don't appreciate the magnitude of what Im wishing for. But I
do think that the first step to making something happen is to
articulate, as clearly as can be done, what it is you want to happen.
One of the beautiful things about working in the software medium is
that if you can imagine something, precisely & consistently, you are
already halfway to creating it.

If anyone in the Scala community is interested to explore the use of
more expressive types in Scala or dialects (especially numerical
bounds/orderings/constraints like my samples), through discussion,
syntactic-thought-experiments, source annotations or compiler plugins,
I'd be interested in collaborating on and/or testing prototype impls.

-Ben

[Daniel Sobral]

You can do it with Church numerals. It's just not easy or fast, but you should find plenty implementations in Scala with ease.

On Tue, Oct 20, 2009 at 10:30 AM, Ben Hutchison <ben@...> wrote:

It finally happened. In recent days, I switched for the first time
from discovering what I _can_ do with Scala to discovering what I
_cannot_.

Ive been thinking about situations in which I know much more about
what code does or should do, at compile-time, than I can express in
Scala's type system.

I present here some example use cases in pseudo-Scala:


//The value returned by this method can be viewed as a subtype of Int,
being a Int between 0 inclusive and bound, exclusive.
val index = random.nextInt(bound: Int): Int{0 <= value < bound}

val smallerArray: Array[Int]{length == bound - 1} = new Array[Int](bound - 1)
val largerArray: Array[Int]{length == bound} = Array[Int](bound)

val elem1 = smallerArray(index)  //compile warning or error
val elem2 = largerArray(index)  //no bounds checking required

abstract class Matrix[Num](val rowCount:Int, val columnCount:Int,
values:Seq[Num]{length >= self.size})  { self =>

 def multiply(other:Matrix): ResultMatrix match {
   //this pattern match determines the method return type!
   case rowCount == other.columnCount => SquareMatrix
   case rowCount < other.columnCount => FatMatrix
   case rowCount > other.columnCount => SkinnyMatrix } = {
     new ResultMatrix(rowCount, columnCount, for (row <- rows; column
<- other.columns) yield row.dot(column))
   }

 def rows:Seq[Seq[Num]] = {...}
 def columns:Seq[Seq[Num]] = {...}
 def size = rowCount * columnCount
}
class SquareMatrix  extends Matrix{columnCount == rowCount}  {}
class FatMatrix  extends Matrix{columnCount >= rowCount}  {}
class SkinnyMatrix  extends Matrix{columnCount <= rowCount}  {}


My knowledge of formal type theory is basic, but I think what is
needed to express the above relations are Dependent Types (types that
depend upon values). A couple of hours internet research suggests that
Dependent Types are a young field with comparatively unexplored
territory.

When I consider how the above pseudo-Scala would execute, I notice that:

1. Tagging objects with a type based on their value works much better
with immutability than mutability, so such techniques might compliment
an Effect System that controlled or tracked mutation.

2. There is a glaring chicken-and-egg problem. The value-dependent
constraints can be threaded through any quantity of dependently-typed
code, but it all has to begin with an entry point from the outside
world, where the first values originate. For example, we might read
the values of a Matrix from a file, and thus have no prior idea about
its row or column sizes.

3. From the implications of point 2, a picture emerges of code that
can be evaluated /at the earliest possible time that its dependencies
are available/. Sometimes this will be at compile time, sometimes once
during runtime initialization, and other times repeatedly during
execution. Compile-time Types and Runtime Values become inter-woven.
At the limit, types describe programmer intent so thoroughly that
typechecking and executing a program converge.


My relative ignorance of type-theory and compiler design means I
probably don't appreciate the magnitude of what Im wishing for. But I
do think that the first step to making something happen is to
articulate, as clearly as can be done, what it is you want to happen.
One of the beautiful things about working in the software medium is
that if you can imagine something, precisely & consistently, you are
already halfway to creating it.

If anyone in the Scala community is interested to explore the use of
more expressive types in Scala or dialects (especially numerical
bounds/orderings/constraints like my samples), through discussion,
syntactic-thought-experiments, source annotations or compiler plugins,
I'd be interested in collaborating on and/or testing prototype impls.

-Ben

--
Daniel C. Sobral

Something I learned in academia: there are three kinds of academic reviews: review by name, review by reference and review by value.

[Donna Malayeri]

You're right that you need dependent types. I think your problem #2 is not really a problem however--it's true that you'd have to insert some run-time checks into your code if you were reading data from some outside source, but type systems can propagate information from the guards in if statements:

val i: Int = readFromFile()
if (i < someBound) {
  ... // in this code, "i" is known to have a particular dependent type, i.e, "< bound"
} else ... // error

Donna

On Tue, Oct 20, 2009 at 2:30 PM, Ben Hutchison <ben@...> wrote:

It finally happened. In recent days, I switched for the first time
from discovering what I _can_ do with Scala to discovering what I
_cannot_.

Ive been thinking about situations in which I know much more about
what code does or should do, at compile-time, than I can express in
Scala's type system.

I present here some example use cases in pseudo-Scala:


//The value returned by this method can be viewed as a subtype of Int,
being a Int between 0 inclusive and bound, exclusive.
val index = random.nextInt(bound: Int): Int{0 <= value < bound}

val smallerArray: Array[Int]{length == bound - 1} = new Array[Int](bound - 1)
val largerArray: Array[Int]{length == bound} = Array[Int](bound)

val elem1 = smallerArray(index)  //compile warning or error
val elem2 = largerArray(index)  //no bounds checking required

abstract class Matrix[Num](val rowCount:Int, val columnCount:Int,
values:Seq[Num]{length >= self.size})  { self =>

 def multiply(other:Matrix): ResultMatrix match {
   //this pattern match determines the method return type!
   case rowCount == other.columnCount => SquareMatrix
   case rowCount < other.columnCount => FatMatrix
   case rowCount > other.columnCount => SkinnyMatrix } = {
     new ResultMatrix(rowCount, columnCount, for (row <- rows; column
<- other.columns) yield row.dot(column))
   }

 def rows:Seq[Seq[Num]] = {...}
 def columns:Seq[Seq[Num]] = {...}
 def size = rowCount * columnCount
}
class SquareMatrix  extends Matrix{columnCount == rowCount}  {}
class FatMatrix  extends Matrix{columnCount >= rowCount}  {}
class SkinnyMatrix  extends Matrix{columnCount <= rowCount}  {}


My knowledge of formal type theory is basic, but I think what is
needed to express the above relations are Dependent Types (types that
depend upon values). A couple of hours internet research suggests that
Dependent Types are a young field with comparatively unexplored
territory.

When I consider how the above pseudo-Scala would execute, I notice that:

1. Tagging objects with a type based on their value works much better
with immutability than mutability, so such techniques might compliment
an Effect System that controlled or tracked mutation.

2. There is a glaring chicken-and-egg problem. The value-dependent
constraints can be threaded through any quantity of dependently-typed
code, but it all has to begin with an entry point from the outside
world, where the first values originate. For example, we might read
the values of a Matrix from a file, and thus have no prior idea about
its row or column sizes.

3. From the implications of point 2, a picture emerges of code that
can be evaluated /at the earliest possible time that its dependencies
are available/. Sometimes this will be at compile time, sometimes once
during runtime initialization, and other times repeatedly during
execution. Compile-time Types and Runtime Values become inter-woven.
At the limit, types describe programmer intent so thoroughly that
typechecking and executing a program converge.


My relative ignorance of type-theory and compiler design means I
probably don't appreciate the magnitude of what Im wishing for. But I
do think that the first step to making something happen is to
articulate, as clearly as can be done, what it is you want to happen.
One of the beautiful things about working in the software medium is
that if you can imagine something, precisely & consistently, you are
already halfway to creating it.

If anyone in the Scala community is interested to explore the use of
more expressive types in Scala or dialects (especially numerical
bounds/orderings/constraints like my samples), through discussion,
syntactic-thought-experiments, source annotations or compiler plugins,
I'd be interested in collaborating on and/or testing prototype impls.

-Ben

[Matthew Willson-3]

The problem with full dependent typing is it requires a turing-
complete type system. Which means there's no way you can guarantee the  
type-checker will terminate.

Say you have a program computing the stream of even numbers which are  
not the sum of two primes, and you assign it the type Stream[Int  
{ value < 4 }]. If the type-checker terminates, hey we've solved the  
goldbach conjecture!

There are systems which can do type-checking of dependently-typed  
programs, but IIRC they mostly take the form of mathematical theorem  
provers / proof assistants. With these you have to do a lot of the  
work yourself in elaborating your program so that it actually acts as  
a rigorous /proof/ that at every stage the values respect the types  
assigned to them. The machine will check your proof, and it can  
provide heuristics and strategies and shortcuts to save you some of  
the work in coming up with that proof, but it needs to be human-
directed to prove anything non-trivial.

Perhaps there is work though on dependent type checkers which can  
infer as much as they can statically in certain more limited  
scenarios, and then give up, leaving runtime assertions in the  
compiled code to check anything which it couldn't infer a proof for at  
compile-time. Which seems (I think?) to be what you're hinting at. I  
think there is some work in this direction on array bounds checking  
for example but I don't know much about it. Would be neat although  
probably a bit insane to attempt in scala alongside everything else,  
just a guess :)

There is a lot of clever stuff you can do in scala though (and even  
more in Haskell) with type-level computation that falls short of  
actual dependent typing.
Eg the stuff with church numerals which has been alluded to. Rather  
than having dependent types that refer to values directly, the  
techniques tend to rely on having type-level values and type-level  
computation going on in parallel to the value-level computation which  
you need to keep a track of. Where the type-level computation acts as  
a proof of the relevant properties of the corresponding values. Can be  
interesting to play with, although can get a bit unwieldy as an  
approach and limited in the kind of tasks which it's practical for.  
Since the kinds of type-level computations expressible aren't turing-
complete (AFAIK in scala!) and can be tricky to encode elegantly.

That said there are some things it's pretty good for, check out  
'metascala' for some examples, I like this one in particular: http://trac.assembla.com/metascala/browser/src/metascala/Units.scala 
  which uses type-level numerals for doing static type-checking of the  
dimensions of physical quantities.

btw: It's a while since I read it, but this is a great (online) book  
on the theory behind dependent types and how it relates to programming:

Programming in Martin-Löf's Type Theory
http://www.cs.chalmers.se/Cs/Research/Logic/book/

-Matt


On 21 Oct 2009, at 00:41, Donna Malayeri wrote:

> You're right that you need dependent types. I think your problem #2  
> is not really a problem however--it's true that you'd have to insert  
> some run-time checks into your code if you were reading data from  
> some outside source, but type systems can propagate information from  
> the guards in if statements:
>
> val i: Int = readFromFile()
> if (i < someBound) {
>   ... // in this code, "i" is known to have a particular dependent  
> type, i.e, "< bound"
> } else ... // error
>
> Donna
>
> On Tue, Oct 20, 2009 at 2:30 PM, Ben Hutchison  
> <ben@...> wrote:
> It finally happened. In recent days, I switched for the first time
> from discovering what I _can_ do with Scala to discovering what I
> _cannot_.
>
> Ive been thinking about situations in which I know much more about
> what code does or should do, at compile-time, than I can express in
> Scala's type system.
>
> I present here some example use cases in pseudo-Scala:
>
>
> //The value returned by this method can be viewed as a subtype of Int,
> being a Int between 0 inclusive and bound, exclusive.
> val index = random.nextInt(bound: Int): Int{0 <= value < bound}
>
> val smallerArray: Array[Int]{length == bound - 1} = new Array[Int]
> (bound - 1)
> val largerArray: Array[Int]{length == bound} = Array[Int](bound)
>
> val elem1 = smallerArray(index)  //compile warning or error
> val elem2 = largerArray(index)  //no bounds checking required
>
> abstract class Matrix[Num](val rowCount:Int, val columnCount:Int,
> values:Seq[Num]{length >= self.size})  { self =>
>
>  def multiply(other:Matrix): ResultMatrix match {
>    //this pattern match determines the method return type!
>    case rowCount == other.columnCount => SquareMatrix
>    case rowCount < other.columnCount => FatMatrix
>    case rowCount > other.columnCount => SkinnyMatrix } = {
>      new ResultMatrix(rowCount, columnCount, for (row <- rows; column
> <- other.columns) yield row.dot(column))
>    }
>
>  def rows:Seq[Seq[Num]] = {...}
>  def columns:Seq[Seq[Num]] = {...}
>  def size = rowCount * columnCount
> }
> class SquareMatrix  extends Matrix{columnCount == rowCount}  {}
> class FatMatrix  extends Matrix{columnCount >= rowCount}  {}
> class SkinnyMatrix  extends Matrix{columnCount <= rowCount}  {}
>
>
> My knowledge of formal type theory is basic, but I think what is
> needed to express the above relations are Dependent Types (types that
> depend upon values). A couple of hours internet research suggests that
> Dependent Types are a young field with comparatively unexplored
> territory.
>
> When I consider how the above pseudo-Scala would execute, I notice  
> that:
>
> 1. Tagging objects with a type based on their value works much better
> with immutability than mutability, so such techniques might compliment
> an Effect System that controlled or tracked mutation.
>
> 2. There is a glaring chicken-and-egg problem. The value-dependent
> constraints can be threaded through any quantity of dependently-typed
> code, but it all has to begin with an entry point from the outside
> world, where the first values originate. For example, we might read
> the values of a Matrix from a file, and thus have no prior idea about
> its row or column sizes.
>
> 3. From the implications of point 2, a picture emerges of code that
> can be evaluated /at the earliest possible time that its dependencies
> are available/. Sometimes this will be at compile time, sometimes once
> during runtime initialization, and other times repeatedly during
> execution. Compile-time Types and Runtime Values become inter-woven.
> At the limit, types describe programmer intent so thoroughly that
> typechecking and executing a program converge.
>
>
> My relative ignorance of type-theory and compiler design means I
> probably don't appreciate the magnitude of what Im wishing for. But I
> do think that the first step to making something happen is to
> articulate, as clearly as can be done, what it is you want to happen.
> One of the beautiful things about working in the software medium is
> that if you can imagine something, precisely & consistently, you are
> already halfway to creating it.
>
> If anyone in the Scala community is interested to explore the use of
> more expressive types in Scala or dialects (especially numerical
> bounds/orderings/constraints like my samples), through discussion,
> syntactic-thought-experiments, source annotations or compiler plugins,
> I'd be interested in collaborating on and/or testing prototype impls.
>
> -Ben
>

[Ben Hutchison]

On Wed, Oct 21, 2009 at 12:41 PM, Matthew Willson
<matthew.willson@...> wrote:
> The problem with full dependent typing is it requires a turing-complete type
> system. Which means there's no way you can guarantee the type-checker will
> terminate.

Acknowledging that I need to learn alot more about dependent types to
be fully informed, I wonder whether this proves a major problem in
practice? Lots of everyday software is not guaranteed to terminate,
yet it does so so reliably enough for normal input to be useful.

>
> Say you have a program computing the stream of even numbers which are not
> the sum of two primes, and you assign it the type Stream[Int { value < 4 }].
> If the type-checker terminates, hey we've solved the goldbach conjecture!

I dont have a sense of what the non-terminating computation the
typechecker would perform here... ?

> Perhaps there is work though on dependent type checkers which can infer as
> much as they can statically in certain more limited scenarios, and then give
> up, leaving runtime assertions in the compiled code to check anything which
> it couldn't infer a proof for at compile-time. Which seems (I think?) to be
> what you're hinting at.

My main motivation is, as a practical programmer, to apply more
expressive or descriptive static types to my code than is currently
possible: narrowing the gap between my mental semantic model and the
semantic model encoded by the programming language. Ive really
stumbled onto dependent types by accident, in that they appear from
several reports to be the tool needed to move static typing to a
higher level.

I do think adaptively switching between static and runtime checking is
fine if it makes the problem tractable.

Would be
> neat although probably a bit insane to attempt in scala alongside everything
> else, just a guess :)

Yes, in that mainstream Scala has been growing rapidly and need some
time to stabilize. However, there would presumably be a considerable
lead time in developing extensions to the typing model, that might
proceed outside the core, in parallel to the language and library
development.


> http://trac.assembla.com/metascala/browser/src/metascala/Units.scala which
> uses type-level numerals for doing static type-checking of the dimensions of
> physical quantities.
>
> Programming in Martin-Löf's Type Theory
> http://www.cs.chalmers.se/Cs/Research/Logic/book/

Interesting. Thanks for the links.

-Ben

[Adriaan Moors-2]

Hi Ben,

On Wed, Oct 21, 2009 at 8:53 AM, Ben Hutchison <ben@...> wrote:

> The problem with full dependent typing is it requires a turing-complete type
> system. Which means there's no way you can guarantee the type-checker will
> terminate.

Acknowledging that I need to learn alot more about dependent types to
be fully informed, I wonder whether this proves a major problem in
practice? Lots of everyday software is not guaranteed to terminate,
yet it does so so reliably enough for normal input to be useful.

Well, it's not really about decidability. To be honest, the main problem is that we (as PL researchers) haven't figured out how to make them user-friendly yet. Sorry! ;-)

The most user-friendly fully-dependently typed language that I know of is Coq.

It's a proof assistant. Enough said, I think.

More seriously, once you unleash that much power in the type system, type inference becomes full-blown theorem proving, which obviously is "very hard". Thus, the programmer has to spell out explicitly quite a bit of the types, and since you express very rich specifications in your types, it also becomes a lot harder to meet them in your implementation. Of course, that's a plus when you're writing software for an Airbus, but it's an incredible feat to do that for any non-trivial program. For example, here's a paper by Xavier Leroy on his verified compiler: http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf

 

Several PhD theses are waiting to be written on how to seamlessly scale a type system from "JavaScript-strength" to "Coq-strength", and how to marry the desires for correct and efficient software (proving a high-level program is hard enough as it is, verifying low-level ones is much harder still, see e.g., http://vcc.codeplex.com/)

cheers

adriaan

[Jesper Nordenberg]

Adriaan Moors wrote:
> Well, it's not really about decidability. To be honest, the main problem
> is that we (as PL researchers) haven't figured out how to make them
> user-friendly yet. Sorry! ;-)
>
> The most user-friendly fully-dependently typed language that I know of
> is Coq.
> It's a proof assistant. Enough said, I think.

Well, it's not very hard to make a user friendly Turing complete type
system with some termination checks (for example C++ templates). I'll
take that any day over a limited type system.

/Jesper Nordenberg

[Adriaan Moors-2]

On Wed, Oct 21, 2009 at 11:14 AM, Jesper Nordenberg <megagurka@...> wrote:

Adriaan Moors wrote:

Well, it's not really about decidability. To be honest, the main problem is that we (as PL researchers) haven't figured out how to make them user-friendly yet. Sorry! ;-)

The most user-friendly fully-dependently typed language that I know of is Coq.
It's a proof assistant. Enough said, I think.

Well, it's not very hard to make a user friendly Turing complete type system with some termination checks (for example C++ templates). I'll take that any day over a limited type system.

Really? User-friendly? Templates? I never thought I'd hear those two in the same sentence :-)

How about modular typechecking? Understandable error messages (ok, ok, we're not there yet in Scala ;-))?   [See Siek et al on Concepts]

My money is on layering (a variation of) open type functions (akin to what's happening in Haskell at the moment) on top of implicits to make them more robust/principled/user-friendly/...

adriaan

[Jesper Nordenberg]

Adriaan Moors wrote:
> Really? User-friendly? Templates? I never thought I'd hear those two in
> the same sentence :-)
> How about modular typechecking? Understandable error messages (ok, ok,
> we're not there yet in Scala ;-))?   [See Siek et al on Concepts]

Ok, calling C++ user friendly is an exaggeration. D is a better example,
it already has concepts (called constraints in D) and nicer syntax for
templates (with static conditionals for example). Basically you have a
nice, generic programming language which is evaluated at compile time.

 > My money is on layering (a variation of) open type functions (akin to
 > what's happening in Haskell at the moment) on top of implicits to make
 > them more robust/principled/user-friendly/...

I'll read up on that.

/Jesper Nordenberg

[Adriaan Moors-2]

On Wed, Oct 21, 2009 at 1:56 PM, Jesper Nordenberg <megagurka@...> wrote:

Adriaan Moors wrote:

Really? User-friendly? Templates? I never thought I'd hear those two in the same sentence :-)
How about modular typechecking? Understandable error messages (ok, ok, we're not there yet in Scala ;-))?   [See Siek et al on Concepts]

Ok, calling C++ user friendly is an exaggeration. D is a better example, it already has concepts (called constraints in D) and nicer syntax for templates (with static conditionals for example). Basically you have a nice, generic programming language which is evaluated at compile time.

Interesting! Must check out D, then. Thanks for the pointer.

adriaan 

[Eric Willigers]

Adriaan Moors wrote:
> To be honest, the main problem
> is that we (as PL researchers) haven't figured out how to make them
> user-friendly yet. Sorry! ;-)
>
> The most user-friendly fully-dependently typed language that I know of
> is Coq.
> It's a proof assistant. Enough said, I think.

Another example is ATS
http://www.ats-lang.org/

> More seriously, once you unleash that much power in the type system,
> type inference becomes full-blown theorem proving, which obviously is
> "very hard". Thus, the programmer has to spell out explicitly quite a
> bit of the types, and since you express very rich specifications in your
> types, it also becomes a lot harder to meet them in your implementation.
> Of course, that's a plus when you're writing software for an Airbus, but
> it's an incredible feat to do that for any non-trivial program.

e.g. the compile-time-checked sort implementation
   http://www.ats-lang.org/EXAMPLE/MISC/listquicksort.dats
is intimidating.