planned type system enhancements

[Dennis Haupt]

hi there,

after 10+ years of using statically typed languages and not having a clue why anyone would use dynamic types because all you get is code you can't maintain, i finally understood one big advantage of dynamic typing (thanks to clojure which was an eye opener).

in java, you force the caller of a method to use an instance of type X - even if you only need a small fraction of X's methods or fields. if you have a big class that can do a lot or provides a lot of information, that class will appear virtually anywhere even though only parts of it are accessed.

in clojure, instead of "i need type x" you say "i need something that is compatible to type x" where type x might never be explicily declared and only exists in the programmers mind and at runtime.

scala has structural types for that, but clojure's destructuring is more powerful. it works on maps, arrays and classes and i won't have to worry about what is given to my function.

the absense of a type system also makes things like
createmap(key, value, key2, value2... keyN, valueN) possible. no typesystem i know of can be told to make sure the number of parameters is _ % 2 == 0. of course you can always cheat by using tuples or method overloading for every possible parameter count up to 2*n but the most simple solution in this case is to just skip the static types.

so i wonder, what are the improvements planned for the next scala releases?

[Tony Morris]

There is a type system you know of that is capable of that. It is called
"Scala" and since you are given greater guarantees of correctness, the
ability to go even higher in abstraction is much more tractable.
Furthermore, not only is this possible, but everything you describe, and
more, also has been implemented.

The most "simple" solution is not to "just skip the static types."

I especially love how "simple" has become a synonym for "this is the
current limit of my capacity."

Don't forget though, Scala is not simple; it is complex.

Do I have to keep taking this stuff seriously?

--
Tony Morris
http://tmorris.net/

[Dennis Haupt]

how does a method signature that enforces an even number of parameters look like? you *have* to use an intermediate structure that combines two parameters into one. or did i miss something?

-------- Original-Nachricht --------
> Datum: Wed, 16 Nov 2011 21:53:15 +1000
> Von: Tony Morris <tonym...@gmail.com>
> An: scala-...@googlegroups.com
> Betreff: Re: [scala-debate] planned type system enhancements

that is actually pretty close to my definition of simple

[√iktor Ҡlang]

On Wed, Nov 16, 2011 at 12:47 PM, Dennis Haupt <h-s...@gmx.de> wrote:

hi there,

after 10+ years of using statically typed languages and not having a clue why anyone would use dynamic types because all you get is code you can't maintain, i finally understood one big advantage of dynamic typing (thanks to clojure which was an eye opener).

in java, you force the caller of a method to use an instance of type X - even if you only need a small fraction of X's methods or fields. if you have a big class that can do a lot or provides a lot of information, that class will appear virtually anywhere even though only parts of it are accessed.

in clojure, instead of "i need type x" you say "i need something that is compatible to type x" where type x might never be explicily declared and only exists in the programmers mind and at runtime.

scala has structural types for that, but clojure's destructuring is more powerful. it works on maps, arrays and classes and i won't have to worry about what is given to my function.

the absense of a type system also makes things like
createmap(key, value, key2, value2... keyN, valueN) possible. no typesystem i know of can be told to make sure the number of parameters is _ % 2 == 0. of course you can always cheat by using tuples

You start out by saying that it cannot be done, and then you say that it's cheating to do it?
That's a nice one!
 

or method overloading for every possible parameter count up to 2*n but the most simple solution in this case is to just skip the static types.

def createmap[K,V](kvs: (K,V)*) //Now that wasn't hard?
 

so i wonder, what are the improvements planned for the next scala releases?

--
Viktor Klang

Akka Tech Lead

Typesafe - Enterprise-Grade Scala from the Experts

Twitter: @viktorklang

[Adriaan Moors]

in clojure, instead of "i need type x" you say "i need something that is compatible to type x" where type x might never be explicily declared and only exists in the programmers mind and at runtime.

I don't follow. I'm guessing you don't really say "i need something that is compatible to type x", you just hope it will be.

Could you be a bit more precise, and show us how Clojure allows you to "say" this, without saying it? It sounds like a koan to me. (Absence of information does not count as "expressing"/"saying" something -- I think we can agree on that, right?)

scala has structural types for that, but clojure's destructuring is more powerful. it works on maps, arrays and classes and i won't have to worry about what is given to my function.

again, I realize we're on debate, but a concrete example would surely make the discussion more enlightening

 

the absense of a type system also makes things like
createmap(key, value, key2, value2... keyN, valueN) possible. no typesystem i know of can be told to make sure the number of parameters is _ % 2 == 0. of course you can always cheat by using tuples or method overloading for every possible parameter count up to 2*n but the most simple solution in this case is to just skip the static types.

what exactly are you saying is possible without a type system, but not with?

i think you're saying:

"not constraining" is possible without [a type system], but 

"constraining" is not possible with [a type system] (admittedly, the type systems you know of)

I don't know of any (sound) logic where the previous implies:

"not constraining" is not possible with [a type system]

whereas I can't immediately come up with a way of statically enforcing the number of args in a variable-length argument be even, I can certainly imagine "not constraining" in Scala, and it's also possible to express lists that statically track their length, although these are not compatible with the syntax you just described...

here's how you can statically track whether a list has an even number of elements -- no casts, dynamic types, or telepathy involved!

:Welcome to Scala version 2.9.1.final (Java HotSpot(TM) 64-Bit Server VM, Java 1.6.0_29).

Type in expressions to have them evaluated.

Type :help for more information.

scala> :paste

// Entering paste mode (ctrl-D to finish)

trait TBool{type Not <: TBool}

trait TTrue extends TBool { type Not = TFalse}

trait TFalse extends TBool {type Not = TTrue }

 

trait IsEvenList[+T]{ self => 

  type IsEven <: TBool

  def ~:[U >: T](x: U): IsEvenList[U]{type IsEven = self.IsEven#Not} =  new ~:(x, this) { override type IsEven = self.IsEven#Not }

}

abstract class ~:[+T](hd: T, tl: IsEvenList[T]) extends IsEvenList[T]

case object NilE extends IsEvenList[Nothing] { type IsEven = TTrue }

type EvenList[T] = IsEvenList[T]{type IsEven = TTrue}

def even[T](xs: EvenList[T]) = xs

// Exiting paste mode, now interpreting.

scala> even(1 ~: NilE)

<console>:14: error: type mismatch;

 found   : IsEvenList[Int]{type IsEven = NilE.IsEven#Not}

 required: EvenList[?]

              even(1 ~: NilE)

                     ^

scala> even(1 ~: 2 ~: NilE)

res1: EvenList[Int] = IsEvenList$$anon$1@6a6fa22b

[Lars Hupel]

> how does a method signature that enforces an even number of
> parameters look like? you *have* to use an intermediate structure
> that combines two parameters into one. or did i miss something?

No, there would be also the possibility to use an HList and an implicit
evidence that the HList of the structure you want (this evidence will
also carry a way to destructure the HList). The implicit search can be
compared to a Prolog interpreter, and the divisibility by 2 is
definitely something it can do.

Furthermore, Scala's type system itself is Turing-complete. You can
encode whatever is computable in types, without even using implicits.
Refer to
<http://apocalisp.wordpress.com/2011/01/13/simple-ski-combinator-calculus-in-scalas-type-system/>
for more information.

[Adriaan Moors]

Furthermore, Scala's type system itself is Turing-complete. You can
encode whatever is computable in types, without even using implicits.
Refer to
<http://apocalisp.wordpress.com/2011/01/13/simple-ski-combinator-calculus-in-scalas-type-system/>
for more information.

yeah, this is cool stuff, but please note that this is exploiting a loophole: type projections like X#ap, where X is an abstract type

I really want Scala to support user-friendly type-level computation, and (if it is up to me) it will be closer to the functional style shown in the SKI example than to implicits, but a lot more research is needed to come up with good termination criteria, nice syntax, clear error messages,... in other words, this is not coming anytime soon, but I'm thinking about it in my copious spare time :-)

cheers

adriaan

[Lars Hupel]

> yeah, this is cool stuff, but please note that this is exploiting a
> loophole: type projections like X#ap, where X is an abstract type

What exactly do you mean by "loophole"? Because `X#ap` is replaced by
the type which it stands for and not left as it is?

[Dennis Haupt]

-------- Original-Nachricht --------
> Datum: Wed, 16 Nov 2011 13:40:47 +0100
> Von: "√iktor Ҡlang" <viktor...@gmail.com>
> An: Dennis Haupt <h-s...@gmx.de>
> CC: scala-...@googlegroups.com

> Betreff: Re: [scala-debate] planned type system enhancements

> On Wed, Nov 16, 2011 at 12:47 PM, Dennis Haupt <h-s...@gmx.de> wrote:

no of course not, but you don't say "even number of parameters" to the type system, you're saying "variable number of tuples having 2 attributes"

you can express this easily in scala, but only with the help of other constructs like a tuple, implicit conversions and other helpers.

what if i make up the following rule:
the first parameter is an instance of type x. the next n parameters are optional parameters and the next one is mandatory and of type z.

the call would look like this in clojure
(magic first op1 op2 op3 last
first2 op1b op2b last2
....)

in scala, the call would look like:

magic((first,List(op1,op2,op3), last), ...)

i need to put the parameters into a structure before making the call. in clojure or a magic static type system more powerful than that of scala, i can just apply them without preparing a structure at every call site. the called function would take care of that, or the magic compiler that i have not seen yet.

>
>
> >
> > so i wonder, what are the improvements planned for the next scala
> releases?
> >
> >
>
>
> --
> Viktor Klang
>
> Akka Tech Lead

> Typesafe <http://www.typesafe.com/> - Enterprise-Grade Scala from the
> Experts
>
> Twitter: @viktorklang

[√iktor Ҡlang]

No, I was even more specific: "a sequence of key-value pairs, where the keys hae type K and the values type V"
 

you can express this easily in scala, but only with the help of other constructs like a tuple, implicit conversions and other helpers.

To express something you must be able to express it, not expressing it doesn't express it.
 

what if i make up the following rule:
the first parameter is an instance of type x. the next n parameters are optional parameters and the next one is mandatory and of type z.

Works just fine:

scala> def magic[A,B,C](a: A)(bs: B*)(c: C) = ()
magic: [A, B, C](a: A)(bs: B*)(c: C)Unit

scala> magic("foo")(1,2,3)("bar")
 

the call would look like this in clojure
(magic first op1 op2 op3 last
      first2 op1b op2b last2
      ....)

in scala, the call would look like:

magic((first,List(op1,op2,op3), last), ...)

i need to put the parameters into a structure before making the call. in clojure or a magic static type system more powerful than that of scala, i can just apply them without preparing a structure at every call site. the called function would take care of that, or the magic compiler that i have not seen yet.

See above.
 

>
>
> >
> > so i wonder, what are the improvements planned for the next scala
> releases?
> >
> >
>
>
> --
> Viktor Klang
>
> Akka Tech Lead

> Typesafe <http://www.typesafe.com/> - Enterprise-Grade Scala from the
> Experts
>
> Twitter: @viktorklang

--

Viktor Klang

Akka Tech Lead

Typesafe - Enterprise-Grade Scala from the Experts

Twitter: @viktorklang

[Dennis Haupt]

-------- Original-Nachricht --------
> Datum: Wed, 16 Nov 2011 14:14:28 +0100
> Von: Adriaan Moors <adriaa...@epfl.ch>

> An: Dennis Haupt <h-s...@gmx.de>
> CC: scala-...@googlegroups.com
> Betreff: Re: [scala-debate] planned type system enhancements

> >

> > in clojure, instead of "i need type x" you say "i need something that is
> > compatible to type x" where type x might never be explicily declared and
> > only exists in the programmers mind and at runtime.
> >
> I don't follow. I'm guessing you don't really say "i need something that
> is

> compatible to type x", you just *hope *it will be.

you "say" it at runtime. as i said, there is no static type system which i know of that can make everything typesafe what i can do with dynamic typing.

[Dennis Haupt]

-------- Original-Nachricht --------
> Datum: Wed, 16 Nov 2011 15:21:41 +0100

it's not the same. the scala call *would*, if possible, be:

magic("foo",1,2,3,4,"bar","foo2",5,6,"bar2")

and it would be the job of the compiler to figure out that the numbers belong together.

[Adriaan Moors]

On Wed, Nov 16, 2011 at 3:22 PM, Dennis Haupt <h-s...@gmx.de> wrote:

as i said, there is no static type system which i know of that can make everything typesafe what i can do with dynamic typing.

yeah, you can keep saying that, and it's true (and i consider that a feature -- i wouldn't want the unsafe things you can do with dynamic typing to be considered typesafe, for one), but I don't see how your statement contributes to the debate

[√iktor Ҡlang]

I beg to differ, the difference is that mine is typesafe and yours is not.
 

--

Typesafe - Enterprise-Grade Scala from the Experts

Twitter: @viktorklang

[Adriaan Moors]

yes, that shouldn't be allowed -- it's not ruled out explicitly in the spec as far as I can tell,

but, in principle the only rule that governs subtyping of type projections is stated in 3.5.2

A type projection T #t conforms to U #t if T conforms to U

so, you can't use this one to "escape" (to the RHS of a type alias selection, or the bounds of an abstract type) from a type projection

it all depends on how you interpret: "If t is defined by a type alias type t = T, then t is equivalent to T."
In my interpretation, "t" does not include all "T#t" (T must be stable), but this should be clarified in the spec. 

implementation-wise, the problem is with normalization (which is an implementation detail -- i don't think it's spec'ed)
it's a bit too eager in replacing type selections by the corresponding type (essentially doing beta-reduction at the type-level)

cheers

adriaan

[Dennis Haupt]

imagine it would be possible to write code that runs at compile time which checks and restructures the parameters applied to a method.

-------- Original-Nachricht --------
> Datum: Wed, 16 Nov 2011 15:26:48 +0100

> Von: Adriaan Moors <adriaa...@epfl.ch>
> An: Dennis Haupt <h-s...@gmx.de>
> CC: scala-...@googlegroups.com
> Betreff: Re: [scala-debate] planned type system enhancements

> On Wed, Nov 16, 2011 at 3:22 PM, Dennis Haupt <h-s...@gmx.de> wrote:

[Adriaan Moors]

http://scalamacros.org/

[Paul Brauner]

I think what you want is structural subtyping (or "static duck
typing") and scala (as well as ocaml) supports it:

scala> def f(x:Any { def yell : String }) = x.yell + x.yell
f: (x: Any{def yell: String})java.lang.String

scala> class Dog { def yell = "woof"; def size = 4 }
defined class Dog

scala> f(new Dog())
res1: java.lang.String = woofwoof

See, f accepts any type that has *at least* yell. It doesn't care that
Dog has also size or that it is a dog.

Paul

[Dennis Haupt]

yes, that's what i said. scala has structural types for that.

-------- Original-Nachricht --------
> Datum: Wed, 16 Nov 2011 16:53:18 +0100
> Von: Paul Brauner <polu...@gmail.com>

> An: Dennis Haupt <h-s...@gmx.de>
> CC: scala-...@googlegroups.com
> Betreff: Re: [scala-debate] planned type system enhancements

> I think what you want is structural subtyping (or "static duck

[Paul Brauner]

Oops, sorry, missed that part.

Paul

[Jesper Nordenberg]

Adriaan Moors skrev 2011-11-16 15:09:
> I really want Scala to support user-friendly type-level computation, and
> (if it is up to me) it will be closer to the functional style shown in
> the SKI example than to implicits, but a lot more research is needed to
> come up with good termination criteria, nice syntax, clear error
> messages,... in other words, this is not coming anytime soon, but I'm
> thinking about it in my copious spare time :-)

What about "pimping" the existing type alias construct to support
specialization:

type X[T] = T
type X[T >: Int <: Int] = Boolean
type X[T >: String <: String] = Int

Kinda similar to Haskell type families and C++ template specialization.

It would allow a trivial definition of a type level equality check:

type Eq[T, U] = False
type Eq[T >: U <: U, U] = True

/Jesper Nordenberg

[Tony Morris]

Let me know if I can help. I'd expect others who'd be interested too.
Perhaps you could put your current thoughts in writing and we could all
do some thinking about it.

[Tony Morris]

This is a well-documented contention in type theory.

Roughly, the purpose of a static type system is to disallow incorrect
programs while allowing correct programs, but it cannot achieve this
perfectly, so trade-offs must be made. So in order to keep the question
interesting, we must alter it by appealing to practicality.

What correct programs does our static type system disallow? Furthermore,
what are the practical implications of these programs being disallowed
and are they worth the trade-off for the correctness guarantees provided
for the other cases? So far, you have only demonstrated correct programs
that our type system does allow -- how uninteresting. As an interesting
aside, try answering these questions in the context of Java's type
system -- yeah exactly, now you know why it's a bit of a joke.

To demonstrate your point, what you'd need to do is provide a correct
program that the type system disallows, is a relatively common use-case
(this is a bit wishy-washy) and also demonstrate what is required in
order to actually express an equivalent of that program (e.g. extra
labour). So far, you're not even close to doing this.

Sound simple enough? Or was that complex enough -- I can never remember.

[Daniel Yokomizo]

IIRC the regular type systems used in CDuce and XDuce can express this
kind of types, because they use regular expressions over types.

> so i wonder, what are the improvements planned for the next scala releases?

Best regards,
Daniel Yokomizo

[Lars Hupel]

> IIRC the regular type systems used in CDuce and XDuce can express this
> kind of types, because they use regular expressions over types.

Yes, exactly. See for example
<http://www.cis.upenn.edu/~bcpierce/papers/xduce-slides.ps> for details.
However, it turned out to be not very practical, because the type
checker needs exponential time in the worst case.

[Daniel Sobral]

Curious... why? Regular expressions can be evaluated in linear time,
though most implementations fail in this regard just to "optimize" for
the common case, and, of course, to allow back references -- which are
not allowable in a regular expression.

--
Daniel C. Sobral

I travel to the future all the time.

[Lars Hupel]

> Curious... why? Regular expressions can be evaluated in linear time,
> though most implementations fail in this regard just to "optimize" for
> the common case, and, of course, to allow back references -- which are
> not allowable in a regular expression.

That's what I thought first, too; if you refer to regular expressions as
defined by "accepted by a finite automaton". Inclusion testing would be
then to simply take two finite automata, make a product automaton with
some end states flipped around and check emptiness.

However, it seems that those regular expression types need tree
automata, mainly because they allow recursion (?). That seems to fall
out of the scope of a normal finite automaton, but not to the degree
where a context-free grammar is needed (where inclusion is undecidable).

[Adriaan Moors]

What about "pimping" the existing type alias construct to support specialization:

type X[T] = T
type X[T >: Int <: Int] = Boolean
type X[T >: String <: String] = Int

Kinda similar to Haskell type families and C++ template specialization.

It would allow a trivial definition of a type level equality check:

type Eq[T, U] = False
type Eq[T >: U <: U, U] = True

yes, pimping is always good -- and this is more or less what I have in mind

I see two main challenges:

- how to get "openness": probably using "late binding" to allow you to override type aliases in subclasses -- think of how you would implement CanBuildFrom as a type member of GenericTraversable

- related to that: the computation model (basically, how to do normalization)

compare this to implicit arguments: they are statically, but "opaquely", threaded through your program, but the compiler only knows at the call site what the concrete types are, and hence what the "result" of solving the constraints is

we don't have such a notion in the compiler for types: when do they have to become known concretely? when can we "pass them around" abstractly, knowing them only by their bounds (these questions can be answered of course)

so, yes, Tony, everyone, I'd very much like to write something up about this and get your input -- just need to also take some time to sit down and write this up, but before I do that, I should probably write something about the virtualizing pattern matcher, for one

[nicola...@gmail.com]

What correct programs does our static type system disallow? Furthermore,
what are the practical implications of these programs being disallowed
and are they worth the trade-off for the correctness guarantees provided
for the other cases? So far, you have only demonstrated correct programs
that our type system does allow -- how uninteresting. As an interesting
aside, try answering these questions in the context of Java's type
system -- yeah exactly, now you know why it's a bit of a joke.

I would like to complete that by another important question:

 how much noise does the static typing adds to the program?

I think dynamically typed language users would be happy to use a statically

typed language that can type check all the programs they want to write without too

much noise. 

There is also a question of the type warranty that your type checker will enforce.

(The precise meaning of "cannot go wrong".)

[Dennis Haupt]

-------- Original-Nachricht --------
> Datum: Thu, 17 Nov 2011 10:51:35 +0000
> Von: "nicola...@gmail.com" <nicola...@gmail.com>
> An: tmo...@tmorris.net

> CC: scala-...@googlegroups.com
> Betreff: Re: [scala-debate] planned type system enhancements

> >
> >

> > What correct programs does our static type system disallow? Furthermore,
> > what are the practical implications of these programs being disallowed
> > and are they worth the trade-off for the correctness guarantees provided
> > for the other cases? So far, you have only demonstrated correct programs
> > that our type system does allow -- how uninteresting. As an interesting
> > aside, try answering these questions in the context of Java's type
> > system -- yeah exactly, now you know why it's a bit of a joke.
> >
> >
> I would like to complete that by another important question:
> how much noise does the static typing adds to the program?
>
> I think dynamically typed language users would be happy to use a
> statically
> typed language that can type check all the programs they want to write
> without too
> much noise.

more precisely, how often do you have to repeat that noise? once at the method declaration? ok then. at each call site? bad.

[Lars Hupel]

> What about "pimping" the existing type alias construct to support
> specialization:
>
> type X[T] = T
> type X[T >: Int <: Int] = Boolean
> type X[T >: String <: String] = Int

+1

Although I'd say this is not exactly the #1 priority. Still, we would be
very happy to see a draft of such a feature whenever you're ready.

[Jim Powers]

On Wed, Nov 16, 2011 at 9:16 AM, Dennis Haupt <h-s...@gmx.de> wrote:

no of course not, but you don't say "even number of parameters" to the type system, you're saying "variable number of tuples having 2 attributes"

The problem with this is?  For the example you're speaking of it certainly gets the job done.  With compile-time checks to boot, sounds win-win to me.

you can express this easily in scala, but only with the help of other constructs like a tuple, implicit conversions and other helpers.

This is a bad thing?

 

what if i make up the following rule:
the first parameter is an instance of type x. the next n parameters are optional parameters and the next one is mandatory and of type z.

the call would look like this in clojure
(magic first op1 op2 op3 last
      first2 op1b op2b last2
      ....)

in scala, the call would look like:

magic((first,List(op1,op2,op3), last), ...)

i need to put the parameters into a structure before making the call. in clojure or a magic static type system more powerful than that of scala, i can just apply them without preparing a structure at every call site. the called function would take care of that, or the magic compiler that i have not seen yet.

Sure, in clojure you forego any way for the computer to help you keep from screwing up, this is a step forward because?  I program in clojure from time-to-time because I have an unhealthy attraction to lisps and I really like lisp macros (yes, I do know about scalamacros, not holding breath though, the SIP is still in progress), but I have no delusions that clojure actually helps me write significant systems.  I prefer not to recall the number if times I either got the arity or the order of arguments wrong when calling functions in clojure (of course only to discover at run-time).  If you want clojure in Scala you certainly can have it:

def magic(first:First,rest:Object*)

This is ever so slightly better than what you can do in Clojure, but not likely to result in a good use of your time.

Elsewhere in the thread you referred to the "noise" of the use of "structures" in your calling sequence as being bad, that seems silly, those structures at the call site convey useful information.

--

Jim Powers