Functional - Sweeney presentation "The Next Mainstream Language"

Author

Sweeney presentation "The Next Mainstream Language"

Paul Rubin

2007-07-26, 4:17 am

This has gotten some attention at LTU and similar places but I haven't
seen any mention of it here, so I thought I'd ask what the c.l.f.
denizens think of it; specifically the assertion that "type inference
doesn't scale".

The presentation is by a game programmer (someone who writes 500 kloc
realtime C++ programs with add-ons that do 500 GFlops of vertex
shading on the PC's graphics accelerator) describing what he wants in
a language. He describes "The Coming Crisis in Computing" (slide 61):
"By 2009, game developers will face CPU's with 20+ cores, 80+ hardware
threads, and >1 TFlop of computing power" plus GPU's with general
computing capabilities.

What he ends up asking for looks like Haskell with dependent types,
though he rejects Haskell itself based on some specific objections
(maybe not that convincing). It's quite an interesting and fairly
quick read, in my opinion.

Links below are to PPT and PDF versions of the same presentation:

http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt
http://www.st.cs.uni-sb.de/edu/semi...docs/sweeny.pdf

Vityok

2007-07-26, 4:17 am

On 26 , 09:41, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
> This has gotten some attention at LTU and similar places but I haven't
> seen any mention of it here, so I thought I'd ask what the c.l.f.
> denizens think of it; specifically the assertion that "type inference
> doesn't scale".
>
> The presentation is by a game programmer (someone who writes 500 kloc
> realtime C++ programs with add-ons that do 500 GFlops of vertex
> shading on the PC's graphics accelerator) describing what he wants in
> a language. He describes "The Coming Crisis in Computing" (slide 61):
> "By 2009, game developers will face CPU's with 20+ cores, 80+ hardware
> threads, and >1 TFlop of computing power" plus GPU's with general
> computing capabilities.
>
> What he ends up asking for looks like Haskell with dependent types,
> though he rejects Haskell itself based on some specific objections
> (maybe not that convincing). It's quite an interesting and fairly
> quick read, in my opinion.
>
> Links below are to PPT and PDF versions of the same presentation:
>
> http://www.cs.princeton.edu/~dpw/po...docs/sweeny.pdf

Well he says that it would be better to have the compiler to perform
more static checks involving array bounds checking and etc. this seems
to me to be somehow addressed in the ADA programming language...
though, i do not have so much of experience with it.

With best regards,
Victor

Jon Harrop

2007-07-26, 4:17 am

Paul Rubin wrote:
> This has gotten some attention at LTU and similar places but I haven't
> seen any mention of it here, so I thought I'd ask what the c.l.f.
> denizens think of it; specifically the assertion that "type inference
> doesn't scale".

Type inference scales just fine. See the OCaml code base, for example.

> The presentation is by a game programmer (someone who writes 500 kloc
> realtime C++ programs

That is equivalent to around 125kLOC of OCaml. There are many bigger
projects already written in OCaml.

> with add-ons that do 500 GFlops of vertex shading on the PC's graphics
> accelerator)

Could write tools in FPLs. See "Accelerator" for .NET, for example.

> describing what he wants in
> a language. He describes "The Coming Crisis in Computing" (slide 61):
> "By 2009, game developers will face CPU's with 20+ cores, 80+ hardware
> threads, and >1 TFlop of computing power" plus GPU's with general
> computing capabilities.

Nothing new here.

> What he ends up asking for looks like Haskell with dependent types,
> though he rejects Haskell itself based on some specific objections
> (maybe not that convincing).

Not at all convincing. He's missed the big points and is focusing on minor
details that will turn out to have little practical relevance. So this is
just a (healthy) fear of the unknown. I did the same thing before we
started using OCaml. After 4 months of actual OCaml work, it was clear that
we would never look back and that my preconceived concerns were completely
invalid.

> Links below are to PPT and PDF versions of the same presentation:
>
> http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt
> http://www.st.cs.uni-sb.de/edu/semi...docs/sweeny.pdf

I see a lot of parallels with the history of scientific computing. Tim is
moving into tera FLOP computing just as scientists start to decommission
their decade-old tera FLOP machines:

http://www.physorg.com/news70844486.html

He cites many of the concerns that I had when we moved our scientific
computing and visualization from C++ to OCaml four years ago. I thought:

1. 31-bit ints can never work (they work just fine, except now they're
63-bit).

2. Bounds checking will cripple performance (it is barely measureable now,
thanks to the memory gap and some subtleties).

3. Low dimensional vectors and matrices ala C++ (code generation in OCaml:
how many "low dimensions" do you need?).

4. Garbage collection is too slow (GC sped up our code's worst case
performance 5 fold).

There is absolutely no point in trying to forsee where the performance
bottlenecks will be in a code base that doesn't even exist in a language
that you aren't intimately familiar with yet. If Tim is serious about this,
he needs to take the plunge and get some relevant non-trivial code written
in one of the modern high-performance FPLs.

I see three interesting avenues that he should explore:

1. Write some serious code (~50kLOC) in one of the high-performance FPLs:
SML, OCaml or F#.

2. Then get a compiler writer on board and address any deficiencies you find
with current FPLs, e.g. better access to C data structures.

3. Use modern FPLs to write better tools and to autogenerate tedious or
error-prone parts of your C++ code base from a higher-level language.

One thing that stands out from my point of view is that he only discusses
Haskell when OCaml is tried and tested for this kind of work but Haskell is
not.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Jon Harrop

2007-07-26, 4:17 am

Neelakantan Krishnaswami

2007-07-26, 7:06 pm

In article <<7x8x93bra7.fsf_-_@ruckus.brouhaha.com>>,
Paul Rubin <> wrote:
> This has gotten some attention at LTU and similar places but I haven't
> seen any mention of it here, so I thought I'd ask what the c.l.f.
> denizens think of it; specifically the assertion that "type inference
> doesn't scale".

He's right, but you still need it. Type inference is essential for
writing small functions that use complex types. For example, here's a
function that takes two folds and produces a combinator for a nested
loop:

let cross fold1 fold2 f init xs ys =
fold1
(fun x acc -> (fold2 (fun y acc -> f x y acc) ys acc))
xs
init

Here's its type:

val cross :
(('a -> 'b -> 'c) -> 'd -> 'e -> 'f) ->
(('g -> 'h -> 'i) -> 'j -> 'b -> 'c) ->
('a -> 'g -> 'h -> 'i) -> 'e -> 'd -> 'j -> 'f

Here's an example of its use:

# cross List.fold_right Array.fold_right;;
- : ('a -> 'b -> 'c -> 'c) -> 'c -> 'a list -> 'b array -> 'c

Notice that you'd have to introduce 3 quantifiers and instantiate 10
type arguments if you didn't have type inference -- enough work to
turn this from a useful little function into a useless one.

However, at large scale type inference is simply not very much
help. This is because programming at scale is all about programming
with abstract data types, and it is impossible to infer abstract types
from the source code.

It's impossible because the answer to the question of which types
should be held abstract and how much information about the
implementation should be revealed is a property of the program's
design, and not of its source code. Your compiler cannot know this
information unless you tell it.

This is why ML uses type inference for individual functions, but as
soon as you step up to using modules, you start writing signature
declarations. Modules are all about type abstraction, and that's
information you have to tell the computer.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

mrd@cs.cmu.edu

2007-07-26, 7:06 pm

On Jul 26, 2:41 am, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
> This has gotten some attention at LTU and similar places but I haven't
> seen any mention of it here, so I thought I'd ask what the c.l.f.
> denizens think of it; specifically the assertion that "type inference
> doesn't scale".

Saying "type-inference doesn't scale" isn't quite right, seeing how
the average-case performance of typical algorithms is quite fast. I
think some work could be done on improving error messages and helping
the programmer understand how types are propagating through the
system.

A deeper matter is that type-inference is undecidable for more
interesting type systems -- such as a dependent type system which
Sweeney discusses briefly. That doesn't make it useless, it just
means it will have to be supplemented with explicit type annotations.

Paul Rubin

2007-07-26, 7:06 pm

mrd@cs.cmu.edu writes:
> Saying "type-inference doesn't scale" isn't quite right, seeing how
> the average-case performance of typical algorithms is quite fast. I
> think some work could be done on improving error messages and helping
> the programmer understand how types are propagating through the
> system.

I think Sweeney was referring to human complexity of managing a
lot of different packages from multiple authors, that had to somehow
communicate type info through inference, not algorithm complexity.
Someone here replied that the external interfaces of ML modules
(forgive me if I got some of that terminology wrong) need to present
explicit type signatures, so maybe that takes care of the problem.

> A deeper matter is that type-inference is undecidable for more
> interesting type systems -- such as a dependent type system which
> Sweeney discusses briefly. That doesn't make it useless, it just
> means it will have to be supplemented with explicit type annotations.

I've never understood why dedicability is that important. I mean it's
well known that the runtime halting problem is undecidable but people
write programs anyway. C++ has undecidable types and it's usually not
a problem. Plain old Hindley-Milner inference can require exponential
time, so people think "well, that's decidable, so fine", but in
practice exponential seems almost as bad as undecidable. The key is
that the badness only happens on particularly obnoxious inputs that
users won't tend to trigger or can figure out how to debug. Even
non-programmers manage to do that in systems like spreadsheets
which can be made to loop.

Joshua Dunfield

2007-07-26, 7:06 pm

Paul Rubin <http://phr.cx@NOSPAM.invalid> wrote:
[...]
>I've never understood why dedicability is that important. I mean it's
>well known that the runtime halting problem is undecidable but people
>write programs anyway.

Well, yes, they *write* programs, but they very rarely check that they
terminate, which is analogous to checking properties specified via types.

[...]
>Plain old Hindley-Milner inference can require exponential
>time, so people think "well, that's decidable, so fine", but in
>practice exponential seems almost as bad as undecidable. The key is
>that the badness only happens on particularly obnoxious inputs that
>users won't tend to trigger or can figure out how to debug.

But undecidability in (e.g.) dependent typing doesn't affect only
contrived pathological cases. For example, linear inequalities over
rationals are decidable; for nonlinear ones, sure, you can have
heuristics that deal with some cases, but AFAIK there's no clear
line (that's significantly beyond linearity/nonlinearity) such that
nearly all useful cases are on one side *and* decidable.

-j.

Paul Rubin

2007-07-26, 7:06 pm

joshuad@cs.cmu.edu (Joshua Dunfield) writes:
> Well, yes, they *write* programs, but they very rarely check that they
> terminate, which is analogous to checking properties specified via types.

Well, if I write a program to compute sqrt(2) to within 0.0001 with
Newton's method, and if it doesn't finish in 5+ seconds then I figure
it's looping or something else is wrong (this happened to me a few
nights ago). So I'm ok with type checking having 3 possible outcomes:

1. Successful type check
2. Unsuccessful type check, print error message showing inconsistency
3. Maximum search depth or time limit exceeded, compiler gives up
with no answer

> But undecidability in (e.g.) dependent typing doesn't affect only
> contrived pathological cases. For example, linear inequalities over
> rationals are decidable; for nonlinear ones, sure, you can have
> heuristics that deal with some cases, but AFAIK there's no clear
> line (that's significantly beyond linearity/nonlinearity) such that
> nearly all useful cases are on one side *and* decidable.

Well, maybe that's the same situation as with mathematics, where there
are lots of statements in PA that are true but unprovable. We keep
doing mathematics and proving what theorems we can and using the ones
we can prove. For dependent types, the answer may be languages with
embedded proof assistants, like Concoqtion. I haven't tried it yet
but it's on my list.

Jon Harrop

2007-07-26, 7:06 pm

Paul Rubin wrote:
> I've never understood why dedicability is that important. I mean it's
> well known that the runtime halting problem is undecidable but people
> write programs anyway.

You don't want to have to run your debugger on your compiler to work out
where and how you made the compiler hang.

> C++ has undecidable types and it's usually not a problem.

Oh yes it is! When my C++ programs started to take 24hrs and 4x my physical
RAM to compile I ditched C++ for OCaml. All non-trivial template libraries
suffer from this problem.

> Plain old Hindley-Milner inference can require exponential
> time, so people think "well, that's decidable, so fine", but in
> practice exponential seems almost as bad as undecidable.

In practice, you don't hit the exponential. Types over 3rd order are rare
and types over 6th order are unheard of. A factor of 2^6 isn't that bad.

> The key is
> that the badness only happens on particularly obnoxious inputs that
> users won't tend to trigger or can figure out how to debug. Even
> non-programmers manage to do that in systems like spreadsheets
> which can be made to loop.

In practice, OCaml's compile times are vastly better than C++'s.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Paul Rubin

2007-07-26, 7:06 pm

Jon Harrop <jon@ffconsultancy.com> writes:
> You don't want to have to run your debugger on your compiler to work out
> where and how you made the compiler hang.

Is that situation worse than with any other theorem prover?

Jon Harrop

2007-07-26, 7:06 pm

Paul Rubin wrote:
> Jon Harrop <jon@ffconsultancy.com> writes:
>
> Is that situation worse than with any other theorem prover?

Exactly. You don't want a full blown theorem prover run on everything you
write. Theorem provers are notoriously bad for hanging.

When you're talking about compilers, you want as much static checking as
possible for your buck but you want it totally unintrusively and as
efficiently as possible. Preferably, you even want the static checks to
result in faster programs (which they often do).

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Paul Rubin

2007-07-26, 10:05 pm

Jon Harrop <jon@ffconsultancy.com> writes:
> Exactly. You don't want a full blown theorem prover run on everything you
> write. Theorem provers are notoriously bad for hanging.

Have you tried Concoqtion? I've been intrigued by it.

Christopher Browne

2007-07-27, 4:17 am

Quoth mrd@cs.cmu.edu:
> On Jul 26, 2:41 am, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
>
> Saying "type-inference doesn't scale" isn't quite right, seeing how
> the average-case performance of typical algorithms is quite fast. I
> think some work could be done on improving error messages and helping
> the programmer understand how types are propagating through the
> system.

I think the reference more likely indicates "nonscalability" at the
human thought level rather than from the perspective of algorithm
performance.
--
let name="cbbrowne" and tld="acm.org" in name ^ "@" ^ tld;;
http://cbbrowne.com/info/spreadsheets.html
"As soon as we started programming, we found to our surprise that it
wasn't as easy to get programs right as we had thought. Debugging had
to be discovered. I can remember the exact instant when I realized
that a large part of my life from then on was going to be spent in
finding mistakes in my own programs."
-- Maurice Wilkes discovers debugging, 1949

Joachim Durchholz

2007-07-27, 8:05 am

Paul Rubin schrieb:
> Links below are to PPT and PDF versions of the same presentation:
>
> http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt
> http://www.st.cs.uni-sb.de/edu/semi...docs/sweeny.pdf

What the heck is "lenient evaluation"?
I see only the same useless definition repeated over and over in Google
results.

Definitions? Consequences?
Or URLs there?

Regards,
Jo

Paul Rubin

2007-07-27, 7:06 pm

Joachim Durchholz <jo@durchholz.org> writes:
> What the heck is "lenient evaluation"?
> I see only the same useless definition repeated over and over in
> Google results.

http://www.google.com/search?q=id90...t+evaluation%22

finds some good results. I can't look at them right now but will try
later.

Joachim Durchholz

2007-07-28, 4:16 am

Paul Rubin schrieb:
> Joachim Durchholz <jo@durchholz.org> writes:
>
> http://www.google.com/search?q=id90...t+evaluation%22
>
> finds some good results. I can't look at them right now but will try
> later.

Ah, I didn't have Id90 in my search terms and got too much noise in the
search results.
Thanks.

Regards,
Jo

Torben Ægidius Mogensen

2007-08-13, 7:10 pm

Paul Rubin <http://phr.cx@NOSPAM.invalid> writes:

> This has gotten some attention at LTU and similar places but I haven't
> seen any mention of it here, so I thought I'd ask what the c.l.f.
> denizens think of it; specifically the assertion that "type inference
> doesn't scale".
>
> The presentation is by a game programmer (someone who writes 500 kloc
> realtime C++ programs with add-ons that do 500 GFlops of vertex
> shading on the PC's graphics accelerator) describing what he wants in
> a language. He describes "The Coming Crisis in Computing" (slide 61):
> "By 2009, game developers will face CPU's with 20+ cores, 80+ hardware
> threads, and >1 TFlop of computing power" plus GPU's with general
> computing capabilities.
>
> What he ends up asking for looks like Haskell with dependent types,
> though he rejects Haskell itself based on some specific objections
> (maybe not that convincing). It's quite an interesting and fairly
> quick read, in my opinion.
>
> Links below are to PPT and PDF versions of the same presentation:
>
> http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt
> http://www.st.cs.uni-sb.de/edu/semi...docs/sweeny.pdf

I agree with many of his points:

- As much as possible should be statically verified.

- Effectful programming doesn't scale to higly parallel/concurrent systems.

- Exceptions everywhere is bad (exceptions should be considered as effects).

But I don't agree lazy evaluation is the right thing. His example of
why laziness is good really only uses that declarations of values can
be in any order, so you can declare a value after its use. I also
don't agree that type inference doesn't scale. His probalem seems to
be with Haskell's numeric classes which give instance errors all the
time (I get annoyed by this too), but that is a feature of the
standard prelude and intricacies of Haskell type classes rather than
type inference per se.

What I would like for game programming is an SML-like language with
the following additions:

- Effects (including exceptions) explicit in type. Higher-order
functions can (in their type) require their functional parameters
to be effect-free.

- A type-class system. Fewer number types so you don't get instance
errors all the time. Allow overlaps and select most specific
instance (allowing, e.g., effect-free types to use an optimized
instance). Specify int to be more specific than real.

- Comprehensions for lists, arrays, databases, etc. Could be tied to
type classes.

- Compiler must be able to verify array accesses within bounds
statically, possibly helped by programmer annotations or checks.

- Support for region-based memory management (in addition to GC)
and/or compiler-checked stack allocation.

- Meta-programming like in Meta-OCaml.

- Guarded equations (like in Haskell).

- Stream-based concurrency, allowing pattern-matching and
comprehensions on streams.

Torben

ezkcdude

2007-08-13, 7:10 pm

On Aug 13, 9:35 am, torb...@app-2.diku.dk (Torben =C6gidius Mogensen)
wrote:
> Paul Rubin <http://phr...@NOSPAM.invalid> writes:
>
>
>
>
>
> I agree with many of his points:
>
> - As much as possible should be statically verified.
>
> - Effectful programming doesn't scale to higly parallel/concurrent syste=
ms.
>
> - Exceptions everywhere is bad (exceptions should be considered as effec=
ts).
>
> But I don't agree lazy evaluation is the right thing. His example of
> why laziness is good really only uses that declarations of values can
> be in any order, so you can declare a value after its use. I also
> don't agree that type inference doesn't scale. His probalem seems to
> be with Haskell's numeric classes which give instance errors all the
> time (I get annoyed by this too), but that is a feature of the
> standard prelude and intricacies of Haskell type classes rather than
> type inference per se.
>
> What I would like for game programming is an SML-like language with
> the following additions:
>
> - Effects (including exceptions) explicit in type. Higher-order
> functions can (in their type) require their functional parameters
> to be effect-free.
>
> - A type-class system. Fewer number types so you don't get instance
> errors all the time. Allow overlaps and select most specific
> instance (allowing, e.g., effect-free types to use an optimized
> instance). Specify int to be more specific than real.
>
> - Comprehensions for lists, arrays, databases, etc. Could be tied to
> type classes.
>
> - Compiler must be able to verify array accesses within bounds
> statically, possibly helped by programmer annotations or checks.
>
> - Support for region-based memory management (in addition to GC)
> and/or compiler-checked stack allocation.
>
> - Meta-programming like in Meta-OCaml.
>
> - Guarded equations (like in Haskell).
>
> - Stream-based concurrency, allowing pattern-matching and
> comprehensions on streams.
>
> Torben

Sounds a lot like Haskell, doesn't it?

Joachim Durchholz

2007-08-14, 4:35 am

Torben Ægidius Mogensen schrieb:
> - A type-class system. Fewer number types so you don't get instance
> errors all the time. Allow overlaps and select most specific
> instance (allowing, e.g., effect-free types to use an optimized
> instance). Specify int to be more specific than real.

There is no common supertype for int and real that's also numeric. I.e.
the semantics are incompatible (precision loss for real subtraction, no
equivalent for real division for ints, etc. etc. etc).

I'd still want have a multitude of numeric types (you *need* all of
them, at least occasionally), but the standard type should be an
unlimited-size int, with the ability to change the default number type
within a lexical context.

> - Compiler must be able to verify array accesses within bounds
> statically, possibly helped by programmer annotations or checks.

*Definitely* helped by programmer annotations.
Static bounds checking is undecidable.

> - Support for region-based memory management (in addition to GC)
> and/or compiler-checked stack allocation.

Still a research area.
I don't know how to give programmers useful control over memory management.

> - Meta-programming like in Meta-OCaml.
>
> - Stream-based concurrency, allowing pattern-matching and
> comprehensions on streams.

Does anybody have URLs where I can read up on these?

Regards,
Jo

Joachim Durchholz

2007-08-14, 4:35 am

ezkcdude schrieb:
> Sounds a lot like Haskell, doesn't it?

No, he wants a strict language.

Regards,
Jo

Torben Ægidius Mogensen

2007-08-14, 8:07 am

ezkcdude <zamir.evan@gmail.com> writes:

> On Aug 13, 9:35 am, torb...@app-2.diku.dk (Torben Ægidius Mogensen)
> wrote:

>
> Sounds a lot like Haskell, doesn't it?

Not really. I don't want laziness as default (if at all) and I do
want effects and exceptions, using a type-and-effect system (where
Haskell uses monads). Also, Haskell does not support explicit and
compiler-checked region or stack allocation, nor does it suport
meta-programming.

Nor do I want Haskell-style layout-sensitive syntax.

But I agree that many of the above features (type classes,
comprehensions, guarded equations) exist in Haskell.

Torben

Torben Ægidius Mogensen

2007-08-14, 8:07 am

Joachim Durchholz <jo@durchholz.org> writes:

> Torben Ægidius Mogensen schrieb:
>
> There is no common supertype for int and real that's also
> numeric. I.e. the semantics are incompatible (precision loss for real
> subtraction, no equivalent for real division for ints, etc. etc. etc).

Reals with sufficient precision can work as bounded integers with no
precision loss, so if you use only +, -, *, div and mod, you can use
integers, but if you use /, sqrt etc., you use reals. Div for reals
can be defined as x div y = floor (x/y) and x mod y = x - (x div y)*y.

I know that I have ignored some numeric issues, but for games
programming, you don't need to worry overmuch about those.

> I'd still want have a multitude of numeric types (you *need* all of
> them, at least occasionally), but the standard type should be an
> unlimited-size int, with the ability to change the default number type
> within a lexical context.

That sounds reasonable, but for games programming, you often need
reals.

>
> *Definitely* helped by programmer annotations.
> Static bounds checking is undecidable.

Indeed. But you can restrict how you access arrays to make it
decidable.

>
> Still a research area.
> I don't know how to give programmers useful control over memory management.

I was thinking of Cyclone-style compiler-checked regions and similar
for stack allocation (if the compiler can't verify safety of stack
allocation through escape analysis, it rejects the program).

>
> Does anybody have URLs where I can read up on these?

http://www.metaocaml.org/

http://citeseer.ist.psu.edu/79871.html

Torben

Joachim Durchholz

2007-08-14, 8:07 am

Torben Ægidius Mogensen schrieb:
> Joachim Durchholz <jo@durchholz.org> writes:
>
>
> Reals with sufficient precision can work as bounded integers with no
> precision loss, so if you use only +, -, *, div and mod, you can use
> integers, but if you use /, sqrt etc., you use reals. Div for reals
> can be defined as x div y = floor (x/y) and x mod y = x - (x div y)*y.

How about fixed-point arithmetic?
That could be made to work with integer arithmetic.

> I know that I have ignored some numeric issues, but for games
> programming, you don't need to worry overmuch about those.

So you want a relaxed "don't bother me with round-off error problems"
floating-point arithmetic.

>
> Indeed. But you can restrict how you access arrays to make it
> decidable.

You can't without crippling the language.
But annotations would do the trick. One could make them part of a type
so you don't have to retype them everywhere.

>
> I was thinking of Cyclone-style compiler-checked regions and similar
> for stack allocation (if the compiler can't verify safety of stack
> allocation through escape analysis, it rejects the program).

Not a good idea. There's enough data that eventually gets written to
disk or otherwise marshalled, escaping all lexical boundaries. You'd be
unable to construct and return a tree data structure, for example.

It would make sense to have annotations that would invoke this kind of
checking for specific data.
I just don't think that this is a comprehensive solution. After all,
sometimes even reference counting is a good solution.

Regards,
Jo

Torben Ægidius Mogensen

2007-08-14, 7:06 pm

Joachim Durchholz <jo@durchholz.org> writes:

> Torben Ægidius Mogensen schrieb:
>
> How about fixed-point arithmetic?
> That could be made to work with integer arithmetic.
>
>
> So you want a relaxed "don't bother me with round-off error problems"
> floating-point arithmetic.

More or less. For games, you don't bother about rouding errors
anyway.

>
> You can't without crippling the language.
>
> But annotations would do the trick. One could make them part of a type
> so you don't have to retype them everywhere.

Annotations need to be verified by the compiler, otherwise they offer
no guarantees. But verification puts strong limitations on the forms
of annotation, so I don't see how this is much different from limiting
the forms of access to an array.

>
> Not a good idea. There's enough data that eventually gets written to
> disk or otherwise marshalled, escaping all lexical boundaries. You'd
> be unable to construct and return a tree data structure, for example.

I was thinking of this as an option alongside GC: GC would be the
default, but for critical code you can ensure specific time and space
behaviour by allocating values on the stack or in regions and make the
compiler check that the values don't survive past deallocation of the
stack frame or region.

> It would make sense to have annotations that would invoke this kind of
> checking for specific data.

That was more or less the idea.

Additionally, linear types might be a good addition: You could use
linear types to ensure single ownership of, say, a file handle, so the
compiler could verify that you close a file after use and that you
don't have two threads writing to the same file without synchronising
(by passing the handle back and forth). Concurrency and linearity
seems to be a good combination.

Torben

Joachim Durchholz

2007-08-14, 7:06 pm

Torben Ægidius Mogensen schrieb:
> Joachim Durchholz <jo@durchholz.org> writes:
>
> Annotations need to be verified by the compiler, otherwise they offer
> no guarantees.

In principle, yes.

However, even run-time checking has its uses.
For example, while it doesn't prove absence of an index error in a
program, it does prove absence of an index out-of-bounds error in a
given program run.
Also, if statically unenforceable annotations are compiled as run-time
checks that abort the computation and throw an exception, they still
guarantee that no computation will ever give a result based on a faulty
index - that's far more useful than simply punting the issue.

> But verification puts strong limitations on the forms
> of annotation, so I don't see how this is much different from limiting
> the forms of access to an array.

Annotations can be plentiful enough to help the compiler around
undecidability issues. Or they could be checked at run time.

Limiting the forms of access is more restrictive on the kinds of code
that you can write.

> I was thinking of this as an option alongside GC: GC would be the
> default, but for critical code you can ensure specific time and space
> behaviour by allocating values on the stack or in regions and make the
> compiler check that the values don't survive past deallocation of the
> stack frame or region.
>
>
> That was more or less the idea.

Makes sense.

> Additionally, linear types might be a good addition: You could use
> linear types to ensure single ownership of, say, a file handle, so the
> compiler could verify that you close a file after use and that you
> don't have two threads writing to the same file without synchronising
> (by passing the handle back and forth). Concurrency and linearity
> seems to be a good combination.

Stuff like that seems to be incorporated in Clean.
I don't know any details though.

Regards,
Jo

Marshall

2007-08-14, 7:06 pm

On Aug 14, 12:14 am, Joachim Durchholz <j...@durchholz.org> wrote:
>
> There is no common supertype for int and real that's also numeric.

I would say the situation is worse than that: there is no real "real"
at all.<sob> And many common operations produce results that
cannot be represented as a finite digit string: sqrt(2).

It seems that there is no happy response to this situation.
(Assuming IEEE 754 makes one unhappy.) It seems that
opting instead for a computer algebra system brings its own
issues. So we're stuck with approximations of reals.

I liked this paper's approach:

http://repository.readscheme.org/ft...w2004/egner.pdf

The idea in short: there are no approximate numbers, only approximate
operations. Thus we have exact+ and approximate+. (Reminds me
of + and +. in OCaml.) So the maximal supertype can be rational, with
int and float subtypes of that, and int32 a subtype of int. Thus
"subtype"
can mean "subset" although that's not everyone's cup of tea. I like
the
fact that this approach makes precise what is an approximation,
as it were.

> I'd still want have a multitude of numeric types (you *need* all of
> them, at least occasionally), but the standard type should be an
> unlimited-size int,

Agreed.

> with the ability to change the default number type
> within a lexical context.

Ooh, that's a bit scary, if I understand you correctly. What
does that buy you?

>
> *Definitely* helped by programmer annotations.
> Static bounds checking is undecidable.

It seems this area would benefit from a better static/dynamic dial
under programmer control.

>
> Still a research area.
> I don't know how to give programmers useful control over memory management.

At the meta level? Or as policy decisions? Certainly malloc/free are
too low
level. Instead being able to specify things like cache policies and
parameters
without affecting program semantics.

>
>
> Does anybody have URLs where I can read up on these?

I'm sure you already know about Erlang.

I've done a lot of programming with publish/subscribe systems, and
am convinced that it's a great way to go, although the area
could use some higher level abstractions. (Probably what I'm thinking
of is similar to what was above described as "comprehensions
on streams.") A fun search string is "stream sql".

Marshall

Joachim Durchholz

2007-08-14, 7:06 pm

Marshall schrieb:
>
> Ooh, that's a bit scary, if I understand you correctly. What
> does that buy you?

Numeric code uses floating-point arithmetic, financial code uses
fixed-point arithmetic.
With conventions like these, both could use the standard operators and
denotations without having to type special casts and operator symbols
everywhere.

Scary? I don't think so. Essentially, a module would simply import the
right numeric module. Just make sure that imports are easily discernible
as such (standard issue with any programming language with a module system).
New only insofar as it might affect the interpretation of literals like
1.2345, but that's far less problematic than interpreting function names
and operator symbols depending on what modules you import.

>
> It seems this area would benefit from a better static/dynamic dial
> under programmer control.

My personal pet would be that everything is just assertions, but some
are marked as "static" (i.e. the compiler will emit an error if it
cannot prove it statically).

>
> At the meta level? Or as policy decisions? Certainly malloc/free are
> too low
> level. Instead being able to specify things like cache policies and
> parameters
> without affecting program semantics.

I'm more thinking about different ways of memory management.
The ladder is:
* Static allocation
* Static allocation in a small number of explicitly managed heaps
* Stack allocation
* malloc/free, no central control over blocks
* Reference counting
* Reference counting with amortized garbage reaping
* Various methods of automatic GC
All of these methods have situations where they are best. Sometimes you
combine them, sometimes combining them doesn't make sense (reference
counting is usually nonsensical if you have automatic GC, particularly
those with delayed reaping).
I'm at a loss even imagining how different memory management methods
could be combined. Not in a systematic manner at least.

> A fun search string is "stream sql".

Will look up. Thanks.

Regards,
Jo

Jon Harrop

2007-08-15, 4:18 am

Torben Ægidius Mogensen wrote:
> - Effects (including exceptions) explicit in type. Higher-order
> functions can (in their type) require their functional parameters
> to be effect-free.

As long as the effects are inferred. What practical problems would this
solve for games programmers though?

> - A type-class system. Fewer number types so you don't get instance
> errors all the time. Allow overlaps and select most specific
> instance (allowing, e.g., effect-free types to use an optimized
> instance). Specify int to be more specific than real.

=> unpredictable performance?

> - Compiler must be able to verify array accesses within bounds
> statically, possibly helped by programmer annotations or checks.

I don't think this is practically important. If you're iterating
sequentially then you use a HOFs with unsafe internals (manually hoisted
bounds checking). If you accessing out of order then cache incoherence
dwarfs the cost of bounds checking.

> - Support for region-based memory management (in addition to GC)
> and/or compiler-checked stack allocation.

Is that worth it?

> - Guarded equations (like in Haskell).

What are they?

> - Stream-based concurrency, allowing pattern-matching and
> comprehensions on streams.

F# already has most of these features and already runs on the XBox, BTW.

I would say that there are many more practically-important features that
FPLs sometimes lack:

- Support for unboxed product types.
- Support for float32 as a storage format in arbitrary data structures.
- Arbitrary-length arrays.
- High-level and efficient OpenGL bindings.
- Linear types.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Torben Ægidius Mogensen

2007-08-15, 4:18 am

Jon Harrop <jon@ffconsultancy.com> writes:

> Torben Ægidius Mogensen wrote:
>
> As long as the effects are inferred.

Indeed. But with an ability to specify constraints on effects as
parts of type declarations, e.g., that two function can not have
effects (read or write) on the same variable.

> What practical problems would this solve for games programmers
> though?

Mostly in combination with concurrency, where you can guarantee
absence of conflicts by restricting the type. But also to ensure that
memoisation functions and similar are only used on pure functions.

Note that effects can be encapsuled: If a function does side-effects
on one of its own local variables but doesn't export any reference to
the variable (in a closure or such), the function can be considered
effect-free from the outside.

>
> => unpredictable performance?

It could indeed make performance sensitive to such thing as adding
side-effects to a function, but I don't think that is a major problem
as long as people are aware of it. It is not as bad as in some OO
implementations where adding a subclass can slow down uses of the
original class.

>
> I don't think this is practically important. If you're iterating
> sequentially then you use a HOFs with unsafe internals (manually hoisted
> bounds checking).

You can make that HOF access the range information once and loop over
that. Or you can use types to ensure that the array range is at least
as large as the range of the index variable, something like the
dependent types mentioned in the originally referred article.

> If you accessing out of order then cache incoherence
> dwarfs the cost of bounds checking.

Removal of bounds checking is not for performance reasons but for
safety: A game should not stop with an error during play, so you must
ensure absense of errors statically.

It is not as bad as it sounds, as you can just add an explicit range
test just before the access to make the compiler see that the index is
in range. And then you can have sensible error-handling code in the
else-branch. I find this a better alternative to exceptions, as it
forces the programmer to think about where things can go wrong.

>
> Is that worth it?

Surprisingly many allocations can be on the stack and even more if you
add regions, so I would say so. Greg Morriset seems to think so when
he included compiler-checked manual region allocation in Cyclone.

>
> What are they?

Side conditions in addition to patterns as found in Haskell (but not
SML), such as

split [] x l g = (l,g)
split (y:ys) x l g | y<=x = split ys x (y:l) g
split (y:ys) x l g | y>x = split ys x l (y:g)

>
> F# already has most of these features and already runs on the XBox, BTW.

Not all games are XBox, but it does seem like a possible starting
place.

> I would say that there are many more practically-important features that
> FPLs sometimes lack:
>
> - Support for unboxed product types.

Agree. I would make all boxing explicit (and require boxing where
needed in recursive data types). This requires MLTon-style
specialisation of polymorphic functions to types, but I would want
that anyway.

> - Support for float32 as a storage format in arbitrary data structures.

I'm not sure what you mean here. If you want the ability to use
standard floats in data structures, I agree. This shouldn't be too
difficult if you abandon the idea that all non-pointers should have
the lsb set. This requires GC information in other places, but it is
certainly doable (especially if you first monomorphize the program).

> - Arbitrary-length arrays.

Agree. But isn't that already the case in most FPLs?

> - High-level and efficient OpenGL bindings.

This is mostly a library issue, but the module/libray system should be
able to support such. I think type classes and MLTon-style
specialisation would go a long way towards this.

> - Linear types.

Agree, as specified in an earlier post.

Torben

rossberg@ps.uni-sb.de

2007-08-15, 4:18 am

On 15 Aug., 10:27, torb...@app-2.diku.dk (Torben =C6gidius Mogensen)
wrote:
>
> I would make all boxing explicit (and require boxing where
> needed in recursive data types). This requires MLTon-style
> specialisation of polymorphic functions to types, but I would want
> that anyway.

This more or less precludes proper seperate compilation, dynamic
linking, first-class polymorphism, existential types, and much more.
Seems far too high a price to pay for hardwiring it into the language
spec.

- Andreas

Hannah Schroeter

2007-08-24, 7:10 pm

Hello!

Jon Harrop <jon@ffconsultancy.com> wrote:
>He cites many of the concerns that I had when we moved our scientific
>computing and visualization from C++ to OCaml four years ago. I thought:

>1. 31-bit ints can never work (they work just fine, except now they're
>63-bit).

Haskell even has full 32/64 bit integers, btw.

>2. Bounds checking will cripple performance (it is barely measureable now,
>thanks to the memory gap and some subtleties).

>3. Low dimensional vectors and matrices ala C++ (code generation in OCaml:
>how many "low dimensions" do you need?).

>4. Garbage collection is too slow (GC sped up our code's worst case
>performance 5 fold).

In fact that's where I once experienced problems with Ocaml. Not GC
speed, but the memory footprint of the process increasing with no
indication that I leaked (referenced) more and more memory in the
program. I.e. seemed like a runtime problem and that was when I was
forced to rewrite that project in C(C++). In fact I did like development
in non-C languages (be it my experiences with ocaml, be it the
experiences with Haskell or Erlang or...).

>[...]

Kind regards,

Hannah.

Jon Harrop

2007-08-24, 7:10 pm

Hannah Schroeter wrote:
> Jon Harrop <jon@ffconsultancy.com> wrote:
>
>
> Haskell even has full 32/64 bit integers, btw.

Yes. Stalin-compiled Scheme is the only FPL to provide both full-size native
ints and OCaml-like performance though.

>
>
>
> In fact that's where I once experienced problems with Ocaml. Not GC
> speed, but the memory footprint of the process increasing with no
> indication that I leaked (referenced) more and more memory in the
> program. I.e. seemed like a runtime problem and that was when I was
> forced to rewrite that project in C(C++). In fact I did like development
> in non-C languages (be it my experiences with ocaml, be it the
> experiences with Haskell or Erlang or...).

This is very interesting. Did you examine the heap to make sure that you
didn't have a memory leak (e.g. unbounded memoization)? I find OCaml's GC
to be unusually aggressive in collecting and its run-time is very memory
efficient.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

rossberg@ps.uni-sb.de

2007-08-24, 7:10 pm

On Aug 24, 10:11 pm, Jon Harrop <j...@ffconsultancy.com> wrote:
> Stalin-compiled Scheme is the only FPL to provide both full-size native
> ints and OCaml-like performance though.

MLton has full-size native ints, too.

Jon Harrop

2007-08-24, 7:10 pm

rossberg@ps.uni-sb.de wrote:
> On Aug 24, 10:11 pm, Jon Harrop <j...@ffconsultancy.com> wrote:
>
> MLton has full-size native ints, too.

I'll try the latest experimental release of MLton and see if I can benchmark
it against OCaml...

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

rossberg@ps.uni-sb.de

2007-08-24, 7:10 pm

On Aug 25, 1:20 am, Jon Harrop <j...@ffconsultancy.com> wrote:
>
> I'll try the latest experimental release of MLton and see if I can benchmark
> it against OCaml...

That surely would be good, but note that MLton had native ints since
day 1, so the new release isn't really relevant in that respect.

Paul Rubin

2007-08-24, 7:10 pm

rossberg@ps.uni-sb.de writes:
>
> That surely would be good, but note that MLton had native ints since
> day 1, so the new release isn't really relevant in that respect.

What about JHC?

Jon Harrop

2007-08-24, 7:10 pm

rossberg@ps.uni-sb.de wrote:
> On Aug 25, 1:20 am, Jon Harrop <j...@ffconsultancy.com> wrote:
>
> That surely would be good...

The latest experimental MLton binary does now run on my machine:

$ time mlton ray.sml

real 0m8.639s
user 0m6.650s
sys 0m1.856s
$ time ./ray 9 512 >image.pgm

real 0m8.608s
user 0m7.215s
sys 0m1.275s

$ time ocamlopt -inline 1000 ray.ml -o ray

real 0m0.460s
user 0m0.415s
sys 0m0.046s
$ time ./ray 9 512 >image.pgm

real 0m4.030s
user 0m3.964s
sys 0m0.013s

Is there a way to enable optimizations with MLton?

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...entists/?usenet

Markus E L

2007-08-25, 7:08 pm

'h12942+nospam AT usenet DOT kitty DOT sub DOT org (Hannah Schroeter)' wrote:

> In fact that's where I once experienced problems with Ocaml. Not GC
> speed, but the memory footprint of the process increasing with no
> indication that I leaked (referenced) more and more memory in the
> program. I.e. seemed like a runtime problem and that was when I was
> forced to rewrite that project in C(C++). In fact I did like development

Yuck. :-). Rewriting something originally designed for OCaml certainly
is no joy.

BTW: Which OCaml version was that? Could the problem be reproduced in
a smaller sample program? Did you file a bug report? I'm saking not to
doubt your experience but just because I'm rather enamoured :-) with
the language (not alone, but) and I'm always listening for problems of
this kind because of risk assessment.

> in non-C languages (be it my experiences with ocaml, be it the
> experiences with Haskell or Erlang or...).

Regards -- Markus

Sponsored Links