Re: [scala] fixed array type

On Tue, Jun 16, 2009 at 03:24:10PM -0700, Balthazar Crowley wrote:

Thanks for the response. Unfortunately, that expression does not 

denote a type. And the type of the thing it does denote is not what is 

required.

Oh, it sounds like you want a dependent type.

That is, the type "Array[Char] of length 140." Right?

  http://en.wikipedia.org/wiki/Dependent_type

You can't have that in scala or any remotely mainstream language, but it 

is one of my fonder hopes for the future.

Dependent types Classes and interfaces may declare properties: immutable

object members bound at object construction. Types may be defined by

constraining a class or interface’s properties. Value properties enable the

definition of dependent types.

For example, the following code declares a class for a two-dimensional

Point class with an add method.

class Point(x: Int, y: Int) {

  def add(p: Point): Point { 

    return new Point(x+p.x,y+p.y); 

  }

}

The class has integer value properties x and y. The add method creates

and returns a new point by element-wise addition. The dependent type

Point{x==0} is the type of all points with x set to 0; that is, all points

along the y-axis.

4.5 Constrained types

Given a type T, a constrained type T{e} may be constructed by constraining

its properties with a boolean expression e.

T{e} is a dependent type, that is, a type dependent on values. The type T is

called the base type and e is called the constraint. For reference types, the

constraint may specify the places at which the object resides.

For brevity, the constraint may be omitted and interpreted as true.

Constraints on properties induce a natural subtyping relationship: C{c} is

a subtype of D{d} if C is a subclass of D and c entails d.

Type parameters cannot be constrained.

4.5.3 Constraint semantics

STATIC SEMANTICS RULE (Variable occurrence): In a dependent type T =

C{c}, the only variables that may occur in c are (a) self, (b) properties

visible at T, (c) final local variables, final method parameters or final constructor

parameters visible at T, (d) final fields visible at T’s lexical place in

the source program.