Lambda the Ultimate

Yeah, my current plan is similar.

1) Record type = module signature = type class. Record value = module implementation = type class instance. An import statement simply brings a value into the current scope.

2) Allow some function arguments to be marked as "implicit". If some call site of the function doesn't specify the value of an implicit argument, it automatically picks up any value of the correct type that is in scope at the call site. If there's more than one eligible value, it's a compilation error and the caller must specify the value explicitly.

I'm not completely sold on associated types, but it does seem like phantom types are the right way to get those, because it's economical and doesn't have any obvious downsides. Thanks for the idea!

Yes implicit function arguments make sense too, and in fact I have already discussed agda instance arguments elsewhere. Agda's instance arguments are actually type arguments, which for my language won't work as all types for functions will be inferred. I'm looking at first class polymorphism so that types only appear in data type definitions, in which case I will have an optional value argument of a specific type. This type is easily determined by the types constructor. This means there can be an optional argument and whether it is the extra optimal argument or not can be determined by type inference.

data Comparable a = MkComparable {
    compare :: a -> a -> Bool
}
int_compare = MkComparable {
    compare = int_less_than
}
float_compare = MkComparable {
    compare = float_less_than
}

int_compare.compare 1 2
float_compare.compare 2.0 3.0

f {MkComparable t} x y = t.compare x y
g {MkComparable t} x y = use t in compare x y

f int_compare 1 2
f float_compare 2.0 3.0
g int_compare 3 4
g float_compare 4.0 5.0

use int_compare
use float_compare
f 1 2
f 2.0 3.0
g 3 4
g 4.0 5.0

Sounds to me that this is more like Scala implicits (which you can totally pass explicitly if you want).

Yes, certainly Scala implicit are even more similar. What this ultimately comes down to is objects vs ADTs, if you compare this style to the mainstream Java style: http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf

I'm not really convinced by his distinction of overloading vs no overloading, especially since he then seems to like instance arguments, which is a form of overloading that is essentially the same as type classes. So it's a bit strange to dislike one and like the other.

ML modules have typings, which in ML uses a different type system from functions, so they are not values, but can be packed as values. This is why ML functors are modules and not functions and have generative semantics. If you want them to have applicative semantics they must be pure. If you also wish them to have associated types the packed instances must also have different types (using phantom types)

But even with this ML functors do not become ordinary functions due to the difference in the type system.

My solution for my as yet unnamed language (suggestions appreciated) is to use a HM variation with compositional principal typings. Here's an example typing:

f x y = z (x + y)

By type inference gets the type:
{z : a -> b, (+) : c -> d -> a} |- c -> d -> b

Where -> is call-by-value pure application

This is not only a principal typing, the type after the turnstile is exactly the HM type where one exists, and any code fragment is typeable independently and the types compose with other fragments resulting in the same type as if the two fragments were typed together.

This enables ML modules to be ordinary records with purity and type restrictions as above, and functors to be ordinary functions. A pure function acts like an applicative functor, an impure function like a generative functor.

What would be your principal typing for

f x y = z x + z y

f x y = z x + z y

{z : a -> b, (+) : b -> c -> d, z : e -> c} |- a -> e -> d

\z . \x y . z x + z y

{(+) : a -> a -> b} |- (c -> a) -> c -> c -> b

let z = \x . x in \x y . z x + z y 

{(+) : a -> b -> c} |- a -> b -> c

z x + z y
{z : a -> b, (+) : b -> c -> d, z : e -> c} |- d

This is compositional, so if later 'z' is lambda abstracted its monomorphic and the two types must unify. If it is defined in a let or top level is is polymorphic and the definition will be generalised, and each fresh instance unified with each of the definitions for 'z'. The typing for the fragment is the same in either case.

I see where you are going, but technically speaking,

{z : a -> b, (+) : b -> c -> d, z : e -> c}

is not a proper context, so what you derive there is not a "typing" in the usual sense. Unless you extend your type system with intersection types in some way, that is.

You could call them intersection types as {z : a -> b, z : e -> c} == {z : (a -> b) ^ (e -> c)}, but as that cannot exist to the right of the turnstile in the type part of the typing I choose not to. The context is simply a multi-set instead of a set, there is no need for an I(^) or E(^) rule.

How do you decide which constraints to simplify? Using Haskell's => instead of your |- (is there a difference?), do you allow inferred constraints to remain, as in:

foo z = show z -- infer this?  Show a => a -> String

On the other hand, it sounds like you get rid of some constraints, as in:

foo z x y = z x + z y -- Simplify 'intersection' of constraints on z... why?

My question is what rule you're using to decide when to eliminate constraints.

Also, do you allow higher rank types to be assigned for z? Can these higher rank types have context components?

"show" is part of a type class, that is something separate... there are no type classes in these examples.

As the simplification, we want HM types, so we follow the HM rules. So normal HM is function arguments are monomorphic, so we unify the different definitions of z in the context when is abstracted.

The context part of the typings are monomorphic. I think you could use higher ranked types (with appropriate annotation), but I want to have type inference, so I prefer the FCP approach http://web.cecs.pdx.edu/~mpj/pubs/fcp.html

My point is that

{z : a -> b, (+) : b -> c -> d, z : e -> c} |- a -> e -> d

is not a valid instance of the typing judgement of the underlying type system, and there couldn't exist a derivation for it (or what would the variable rule be in such a system?). Hence this is not a typing, and I would avoid using the term principal typing for this.

I disagree this is a compositional principal typing, and the variable rule is simple:

x

{x : a} |- a

As its compositional a variable is assigned a fresh type variable, which is put in the context. This is a perfectly valid typing judgment in the type system I am using, which is an extension of HM types, such that the type (on the right of the turnstile) is always the same as the HM type (if it exists).

Why do you think it is not a valid type judgement?

If you take your example, then for this to be a typing it would have to define a valid type derivation for f, i.e.:

{z : a -> b, (+) : b -> c -> d, z : e -> c} |- \x y -> z x + z y : a -> e -> d

That doesn't work, certainly not with the rule you just gave.

I dont understand your objection. Here is the complete compositional derivation for \x . \y . add (z x) (z y) I have changed the syntax to work with the parser:

var ---------------------------------------
add : {add : a} |- a

var ---------------------------------------
z : {z : a} |- a

var ---------------------------------------
x : {x : a} |- a

z : {z : a} |- a
x : {x : a} |- a
app ---------------------------------------
(z x) : {x : a, z : (a -> b)} |- b

add : {add : a} |- a
(z x) : {x : a, z : (a -> b)} |- b
app ---------------------------------------
(add (z x)) : {add : (a -> b), x : c, z : (c -> a)} |- b

var ---------------------------------------
z : {z : a} |- a

var ---------------------------------------
y : {y : a} |- a

z : {z : a} |- a
y : {y : a} |- a
app ---------------------------------------
(z y) : {y : a, z : (a -> b)} |- b

(add (z x)) : {add : (a -> b), x : c, z : (c -> a)} |- b
(z y) : {y : a, z : (a -> b)} |- b
app ---------------------------------------
((add (z x)) (z y)) : {add : (a -> (b -> c)), x : d, y : e, z : (d -> a), z : (e -> b)} |- c

((add (z x)) (z y)) : {add : (a -> (b -> c)), x : d, y : e, z : (d -> a), z : (e -> b)} |- c
abs ---------------------------------------
(\y . ((add (z x)) (z y))) : {add : (a -> (b -> c)), x : d, z : (d -> a), z : (e -> b)} |- (e -> c)

(\y . ((add (z x)) (z y))) : {add : (a -> (b -> c)), x : d, z : (d -> a), z : (e -> b)} |- (e -> c)
abs ---------------------------------------
(\x . (\y . ((add (z x)) (z y)))) : {add : (a -> (b -> c)), z : (d -> a), z : (e -> b)} |- (d -> (e -> c))

That is the type inference algorithm. What are the declarative rules defining your type system? The two are not to be confused, and the notion of typing is defined in terms of the latter.

As it is constructive the inference algorithm can also be read as the declarative rules (okay there's stuff missing like how the typing unification works, and how lets work).

It seems to fit within J.B.Wells definition of a typing: "A typing t is defined to be a pair (A ⊢ τ) of a set A of type assumptions together with a result type τ. The meaning Terms(t) of a typing t = (A ⊢ τ) in a particular type system is defined to be the set of all the program fragments M such that A ⊢ M : τ is provable in the system"

The type system is similar to those of Olaf Chitil, and Grego Erdi.

As it is constructive the inference algorithm can also be read as the declarative rules.

No, it can't. How would it derive the equivalent of x : Int ⊢ x : Int, to give a trivial example? Your rules will supposedly always assign a fresh variable as type to a free-standing x.

Note how Well's definition refers to a judgement A ⊢ M : τ relative to which a typing is defined, which is what I was referring to as "the actual type system".

I suggest to read Well's paper more carefully. In particular, he even proves the theorem that HM does not have principal typings.

Have you read Grego Erdi's PhD thesis? Saves me pasting a lot of text here.

The type system is not actually HM, and Well's comments do not directly apply. (Edit: This following is irrelevant, its the multi-set contexts that make the difference) Because there is no polymorphic environment, the typings do represent all possible typings. For example:

x

{x : a} |- x : a

represents all possible typings for 'x'. How about:

x x 

{x : a} |- x : a
{x : a} |- x : a
----------------------
{x : a -> b, x : a} |- x x : b

This represents a simple use of the application rule. Something like:

M' |- E : t'     M'' |- F : t''
-----------------------------
        M |- E F :: t

where
    new a
    SUBS = t' unify (t'' -> a)
    M = SUBS(M' multi-set-union M'')
    t = SUBS(a)

Edit: Re-reading Erdi's thesis, It seems I am doing something different. Erdi still appears to have a polymorphic environment and is not using a multi-set for the context. It would appear what I have is somewhere between HM and Rank-1 intersection types.

Because there is no polymorphic environment, the typings do represent all possible typings.

Is this the crux of it? The lack of a polymorphic environment? Or is it that if we allow multi-set contexts, then HM suddenly does have principal typings? Looking at the proof of Wells here in appendix 4.4, the example term with no principal type is (x x). The proof begins by considering the form of A(x), the single type for x in context A.

For the declarative typing rules that Andreas wanted, what if we just take all of the usual rules of HM, but extended to multi-set contexts? It sounds like you're taking the Abstraction rule to require that the closed-over variable have a single type in the context, and presumably you'd do the same thing for the Let rule, but with polytypes. Is there some problem with doing that? And if you do that, do you get principal typings?

PS. Can you provide a link to Grego Erdi's PhD thesis?

Edit: Ignore my edit ... generalizing over these multi-sets would require more proper intersection types and would be more complicated.

Thinking about it more, it looks straightforward to recast algorithm W to produce typings for HM generalized to multi-set contexts that I think would be principal. Am I wrong? Maybe I'll try implementing it and see what happens.

For let bindings you know the LHS type, which you normally generalise. In this case you take a fresh instance (IE the LHS type with fresh type variables for all free variables) for each occurrence of the symbol in the environment and unify with each occurrence. This unification produces a fresh context. You merge all the contexts together from the unifications to give the new context for the let bound term, the type is that of the RHS with substitutions applied (from all unifications in the context) as normal.

http://gergo.erdi.hu/projects/tandoori/Tandoori-Compositional-Typeclass.pdf

My own understanding, having implemented Kfoury and Wells' System-I and System-E, as well as HM algorithm W, and this compositional algorithm, is that the let rule does behave like a let rule for rank-1 intersection types - however because intersections cannot occur in the types unification is decidable.

Re-reading Erdi's thesis, I don't see him using multi-set contexts, so I think there is some difference between what I am doing and what he did.

In which case I probably have to write down the typing rules.

Edit: I have had a go at writing down the typing rules, and started a new thread to discuss them.

I have posted the type derivations in a new thread, so we can discuss them there. As Matt points out above, Well's proof assumes a single type for 'x' in the context, a restriction I don't have.

No idea what it does but I somewhat can see what the inference rules behind the derivation are.

-

I may be be misunderstanding things, but I was referring to page 5 of this paper. A quote:

The delimcc library may also be understood as generalizing exceptions, a wide-spread and familiar feature. Intuitively, a value of type 'a prompt is an exception object, with operations to pack and extract a thunk of the type unit -> 'a. The expression new_prompt () introduces a new exception object; take_subcont p (fun _ () -> e) packs fun () -> e into the exception object denoted by the prompt p, and raises the exception. The expression push_prompt (fun () -> e) is akin to OCaml's try e with ... form, evaluating e and returning its result. Should e raise an exception p, it is caught, the contained thunk is extracted, and the result of its evaluation is returned. All other exceptions are re-raised.

Basically the "exception types" (the things you mention in "throw" and "catch" statements to establish a point of communication between them) are values, rather than types. You can think of them as cells containing typed continuations, or something like that. I think that's actually more intuitive than having "catch" do type-directed dispatch on the exception's type.

No idea what he's grappling at but the observation is that now somehow the exception made it into the function type declaration.

You really, really, really don't want or need that.

With type inference you never have to specify the function type signature and I want to track side effects like exceptions through the type system. I can see no problems with having it in the signature, and this allows the "main" function to be forced to have no exceptions which means the compiler can statically prove that all exceptions that could possibly be thrown are caught.

Well. If you really want it you can do it. It just goes contrary to experience. It isn't induction. 0 exception declarations is good, 1 is good, 2 is good, ..., n is good. It just stops at two, more is a nuisance.

It'll break compositionality of modules. Change a rule in an imported module (type signature) and you'll need to change either how that is handled or what you export.

And then you'll quickly observe that exceptions tend to propagate both vertically and horizontally throughout modules.

Horizontally since very often definitions are implemented in terms of other definitions of the same module. You'll end up feeling that you should write either the exception for each definition in the module or just as something everything in the module can throw because of orthogonality.

Vertically since you might feel like restricting yourself to declaring one exception possible for the whole module. You'll end up handling, but mostly wrapping, all other exceptions which may be thrown by the other N modules you import; which just means an enormous amount of code.

It's a lousy idea to explicitly declare all exceptions. Even Java doesn't do that though it makes it seem so.

Unlike Keean, I agree with you that checked exceptions are a bad idea. I think value-level exception handling shouldn't necessarily lead to declaring exceptions in every function's type. The alternative (being able to throw anything from anywhere) seems better to me, since I'm mostly interested in imperative languages anyway.

I agree that having to change module signatures would be problematic. It may be that it is better to keep it to simple can throw or cannot, and not actually care what the exception is.

It'll break compositionality of modules.

Works fine if every definition has an inferred exception variable. Pure functions raising no exceptions are then simply a special case that unify with a unit-like exception type, analogous to how functions that return no value, return unit.

Edit: and it's interesting to note that functions that return unit are by and large side-effecting functions, which means they'd have a non-unit exception type; conversely, functions with unit exception types will necessarily have non-unit return types (except for trivial and useless functions that do nothing with their arguments and simply return unit). There's an inversely proportional relationship here that is nicely captured by simply unifying all return types, including exceptions, as a sum, but then you're into territory that marco detests, namely using monadic idioms to thread exception values to their corresponding handlers.

The module types can be polymorphic over the exception type, so that way you can keep the knowledge about thrown exceptions in the type system, but let the compiler infer the actual types thrown. The module type signature could look like:

f :: a -> Exception e () -- function throwing 'e' and returning unit.

When compiling the compiler would substitute the actual type of e inferred from the definition of 'f'.

If you have function types and record types, then you don't need interfaces either. Modules etc. can be just records containing functions. As a bonus, records can contain values as well. For example, an instance of Num probably needs to contain zero and one (the additive and multiplicative identities), to make operations like sum and product work more intuitively on zero-length lists. It seems more natural to have zero and one as values rather than zero-argument methods.

They are semantically equivalent to stuffing values into records. The instances I described can also just hold constants. (Well, I think they can. Never tried. Maybe they'll blow up the compiler, no idea.)

I don't see a reason to add zero and one.

Maybe adding zero and one to Num is not the best example. My motivating examples are more mathematical:

GENERIC(Type) RECORD Group(
  operation: FUNCTION(Type, Type): Type,
  inverse: FUNCTION(Type): Type,
  identity: Type
)

GENERIC(Type) RECORD Field(
  addition: Group(Type),
  multiplication: Group(Type)  # throws on divide by zero
)

GENERIC(Scalar, Vector) RECORD VectorSpace(
  scalars: Field(Scalar),
  vectors: Group(Vector),
  scale: FUNCTION(Vector, Scalar): Vector
)

It just seems intuitive that Group should contain the identity value, and VectorSpace should contain the scalar field and the vector addition group.

Haskell does this and that may be okay-ish for math though I think they got the name binding over type class 'methods' reversed. You're just not going to do a lot with the fact that something is a group except for write simple functions over it you'll get right immediately anyway for concrete instances.

Nobody encounters problems like this in ML or other languages. It doesn't buy you a lot. You might want to express that fold works on all containers but a container is a value. (And then you're going to specialize that function anyway.)

It. Just. Doesn't. Work.

It's just a lousy idea to approach writing software. At best, it tickles programmers interest and you end up with a language good for mathematical computations or mathematical prototypes.

(I am reading the Go sources at the moment. Still looking for the attribute grammars (that's there), the monads and the monoids.)

It. Just. Doesn't. Work.

Not sure I agree. I see applications of these techniques everywhere now, e.g. while translating C++ generic programming idioms to Java in this post. Basically I wanted to express the idea that forward iterators are sometimes also random access iterators, but the conversion makes sense only if random access operations are O(1):

interface Forward<Iterator> {
    Iterator increment(Iterator iterator);
    boolean equal(Iterator first, Iterator second);
    /* Nullable */ RandomAccess<Iterator> getFastRandomAccess();
}
    
interface RandomAccess<Iterator> {
    Iterator add(Iterator iterator, Integer delta);
    Integer subtract(Iterator first, Iterator second);
}

In a better language, Forward<Iterator> would contain a Maybe<RandomAccess<Iterator>> value, not a method that returns a nullable pointer to one.

That's pretty much the point Alex Stepanov was making in his famous interview, that algorithms are defined on algebraic structures, therefore a language that supports generic expression of efficient algorithms must also support expression of algebraic structures, and allow third party code to define new instances of these structures. For example, when I add a new native array type to my language, I want to reuse the quicksort that I already have, not write a new one. Right now it seems to me that "value-level programming" is a perfect fit for what Stepanov wanted.

I see Donads everywhere too these days. House, car, shop, aircraft carrier. It's just an illusion which I don't need to create things and certainly won't put central. (Rummaged through my house. You can add washing machine, closet, and garbage can now too.)

Of course algorithms are defined on algebraic structures. But you're not going to do an awful lot with that.

Going back to the monad example. (Sorry for that.) But I see something where the laws a) are not used for compiler optimization, b) will be broken in an instant, and c) are something I'll just reuse in various manners.

Or going to fold. Something where you can factor out that it's something over a monoid. Big deal that that gives me a general implementation. For any vector I'll just go directly to it's concrete implementation and implement an optimized algorithm for it.

I agree on the value level programming.

I agree that we should avoid overengineering. These translation exercises are more about testing whether value-level programming works for different use cases.

There's no need to go directly to the implementation, there are a series of abstractions, forward_iterator, reversible_iterator, random_access iterator etc...

With a vector there is no performance advantage to not using the random_access_iterator.

So an in-place sort might depend on a mutable random_access iterator, and you are free to implement a new container type that provides those interfaces.

This was one popular misconception in the early days of FP too. It won't help much to implement fold or sort directly when you've got iterators I agree. And C/C++ is very good at implementing fast data structures.

Upto the point where you end up doing computations over very large data sets and you find out that implementing it directly over the array of buckets buys you two orders. A hundred fold increase.

Stuff like this just pops up in a lot of programs. It's the reason I'll not finish my bootstrap any time soon. The language lacks fast primitives.

So in C++ the random_access_iterator is just some static type wrapping around a pointer. The actual implementation is a pointer with add and subtract, so you effectively define '+', '-'. To quote Stepanov, "random-access-iterators provide the full power of computer addresses". So there is zero performance penalty for using one.

That I'll buy

In a pure language a zero argument function is the same as its result value. There is no difference:

f = 3

can be considered a zero argument function or a value, both have the same type Int

With impure functions this is not the case as you need to generate the side effects every time the function is called. We can call pure functions applicative (because they apply to their arguments, and the results are always the same for the same arguments, and hence can be memoised), whereas impure functions have to generate their side-effects every time they are called. This means we have to either ban zero argument impure functions or have a special syntax for calling them. If a curried impure function generates side effects on the application of arguments other than the last. Consider a function which reads a string from stdin, then appends a string supplied as an argument, then prints the result. You may want to call the first part several times, and then apply different arguments, and then print the final string at some later time. If we define '@' as generate side effect of a zero argument function, you might want to do:

a = @f      // read a string from stdin
b = @f      // read a different string from stdin
c = a "hello"   // append hello to the first string
d = a "goodbye"
e = b "hello"
f = b "goodbye" // append goodbye to the second string
@c // print appended strings
@d
@e
@f

dialog:
> jim
> fred
fred hello
fred goodbye
jim hello
jim goodbye

This explains what I was talking about in another thread, where I called impure functions "generative", in that they create a new different intermediate function every time they are applied (as in applying f twice above.

This explains what I was talking about in another thread, where I called impure functions "generative", in that they create a new different intermediate function every time they are applied.

I don't think that is a useful way of talking about it, unless you have a language where functions have observable identity (which in sane languages they don't).

You've been using the words 'generative' and 'applicative' in ways that I find awkward.

I've heard and used the word 'generative' in phrases like 'generative grammar based computation'. In this case, the idea is that we use a grammar to generate a sentence (or story, or geometry, etc.), rather than recognize one. We have generative vs. analytic applications of a grammar. Grammar description languages are rarely equally balanced for both generation and analysis. Generative would also be appropriate for describing how we obtain samples from a probabilistic model, tests from a QuickCheck instance, and so on.

`Applicative`, OTOH, I typically hear in opposition to `combinatoric` (e.g. based on combinators instead of lambdas) or sometimes `concatenative` (~ associative combinators). In applicative languages, we apply a function or operator to some arguments. In combinatorial languages, we only combine or compose functions. Fixpoint combinators would be the counterpoint to recursive applications.

All this seems orthogonal to purity, and pretty far removed from how you're using the words.

I think he uses these words in analogy with generative and applicative functors.

My hypothesis is that applicative functors must be pure, and impure functors must be generative. If a function is a functor (IE where modules are regular datatypes and first class values) then functions must be applicative and generative too, and impure == generative, pure == applicative.

I see, this is about some ML-specific idioms and terminology.

This is a nit, and veering OT, but I find the phrase "generative grammar" difficult to parse. Formal grammars (regular, context-free, context-sensitive, etc.), which consist of production rules, simply are generative. In this context "generative" is redundant. The notable exception in the area of parsing is the class of parsing expression grammars (PEGs, packrat parsing) which are remarkable precisely because they are based on recognition instead of generation. So at least when I see "generative grammar" I read it as emphasizing the exclusion of PEGs.

I get the sense that by using "generative" to modify "grammar", your intent is to emphasize that you mean something other than the grammars you would use when doing parsing applications. Yet, technically, the term "generative grammar" would seem to include the bulk of those.

The choice for this value-level representation was that, in general type level instances are more general, but most of the time you'll never use a type level interface without a value of the appropriate type being present.

It can't express everything but it will express 65% of what you want. (Where 30% you miss is not being able to have containers over different orderings, something I probably should fix once, and the other 5% probably doesn't matter.)

I think the problem with containers is solvable on the value level, this comment gives three possible solutions. More generally, I'd be interested in seeing other problems that seem hard to solve on the value level.

Anyone got a well-founded opinion on that one? The only thing I observe is that Haskell tried the second one and that leads to the worst written and unmaintainable code possible in the world at present. Then again, it might work for Agda. No idea.

My opinion is based on performance and the compiler technology. I think values can depend on values or types, but types should only depend on types. Types should never depend on values. This keep the arrow of time pointing in the right direction, and we can optimise the types away in compilation.

This means instance selection occurs by type, and they type-signature of every instance needs to be different.

This is important because the cost of dynamic dispatch on a modern general-purpose out-of-order super-scalar CPU is about 8 times the cost of a direct function call. This is a huge performance difference, so it is important for the compiler to resolve as many function calls as possible into direct calls, which is done by abstract partial evaluation, otherwise known as type-inference.

So you want values to depend on types as much as possible for performance.

Where you do want types to depend on values for dynamic polymorphism, this should be limited to run-time unknowns, and virtual function dispatch via a virtual function table is faster than using case on a tagged-value.

Indirection buys you abstraction. You will never be able to create a usable abstraction over anything if you want to compile out all the indirection, be it on values or types.

Virtual function tables and tagged values are implementation details, a function table is abstractly a case switch over a pointer represented type.

Lots of polymorphism is static. Consider parser combinators. The combinators are polymorphic but the gammar is statically determined at compile time. Nearly all the parsers can be directly called or inlined by the compiler.

Whether the polymorphism is static or dynamic has nothing to do with abstraction. Consider a vector if integers, although a vector is abstract and polymorphic, if you know it will contain integers you can statically determine all the function calls and call them directly or inline them.

In a static type system _all_ calls are statically determined by type. The only runtime polymorphism comes from pattern matching on disjoint union datatypes.

In a static type system _all_ calls are statically determined by type. The only runtime polymorphism comes from pattern matching on disjoint union datatypes.

Not with first-class polymorphism.

Im not sure about this. I think there are some systems with first-class-polymorphism where you can determine statically at compile time, like FCP. In FCP you pass the polymorphic type as a datatype, which means to use it you must unpack with the type constructor, which gives you the polymorphic type, but you must apply that to other types which result in a ground type known statically at compile time?

Is there a good example of where first-class-polymorphism is not statically typeable, without using polymorphic-recursion? I could do with a good example for my unit-tests.

Nor with polymorphic recursion, as we discussed before. On the other hand, pattern matching has nothing to do with polymorphism (except perhaps if you are dealing with GADTs, which imply first-class existentials).

One counter example does not disprove the concept. Most of the time most things can be statically determined. Although it seems to be accepted that such things are static, perhaps these things go against the original intent of "static" typing? It would be interesting to look at the history and see when concepts that 'break' the static-ness were introduced, and if their originators anticipated that the result would be no longer being able to statically determine all types?

Interestingly I came across the polymorphic recursion problem again recently. With parser-combinators you can do almost everything with static polymorphism, except when a parser calls itself recursively... But this although it happens is not that common. For example with an expression parser there is one rule that needs to be recursive, everything else can be statically determined.

As for pattern matching, it has a lot to do with polymorphism. It is data polymorphism in the same sense as an OO class hierarchy. The datatype is the base-class and each type constructor in the disjoint union is a sub-class. In this way pattern matching serves the same purpose as virtual functions in OO. In fact Ada calls its dynamic polymorphism 'tagged types'.

If we have a datatype like:

data Test = I Int | F Float | S String
list = [I 6, F 3.0, S "hello"]

The list test can contain any type of Int, Float or String, and we can iterate through the list performing actions based on the type of the value by pattern matching on the constructor. This sure looks a lot like polymorphism.

One counter example does not disprove the concept.

Well, all we are pointing out is that it disproves what you said (you even emphasised "_all_").

perhaps these things go against the original intent of "static" typing?

No, it means that checking is static, not that all types can be monomorphised. I think you are the only one trying to define 'static' that way. (Ignoring the fact that the "originators" -- whoever they are -- would probably never use the tautological term "static typing" in the first place.)

we can iterate through the list performing actions based on the type of the value by pattern matching on the constructor. This sure looks a lot like polymorphism.

It may look like it, but technically it is not. Matching is based on the tag, which is independent of types. Variant tags have no more an immediate connection to polymorphism than the dual notion of record labels has. Consider:

type t = {i : int, f : float, s : string}
list = [\r : t -> intToString r.i, \r : t -> floatToString r.f, \r : t -> r.s]

Would you say that the above involves polymorphism, because I happen to be able to give different types to different labels? (In particular, note that records can encode variants.)

Yes, you are right I should have said most and not all. What I meant by the 'intent' of static typing is not well expressed. I can't help feeling that polymorphic recursion is not a natural way to achieve runtime behaviour that depends on values. The languages were designed with datatypes, and pattern matching as a simple clear and obvious way to vary control flow depending on runtime values. You may be able to do things using polymorphic recursion, but you don't need to, and I think it is much clearer and simpler to just use a datatype. If you want to check whether 'x' is less than 3, you should just check the value in an if statement, not lift it to the type level via polymorphic recursion and try and constrain is using Peano typing at the type level. On the other hand static constraints that need to be at compile time you have no other way to achieve this.

As for the list example its just storing a bunch of monomorphic functions of type t -> String so its not polymorphic in the sense I was misusing the word. I was talking about type dependent behaviour. Yes it is technically not polymorphism, but you can achieve the same thing, namely behaviour that depends on the type of the value. Okay you have a value-level tag that tells you which type you actually have, but then thats exactly how boxed types work in polymorphic functions behind the scenes.

I can't help feeling that polymorphic recursion is not a natural way to achieve runtime behaviour that depends on values.

Nonsense. I suppose parametric polymorphism also looks unnatural to a C programmer (... and look at all those hard-to-regain optimization opportunities!).

Polymorphic recursion has the quality of Platonist abstract ideas: it is there, whether it makes your life complicated or not. Whether your language allows it, forbids it or hides it under the carpet is a design question, but polymorphic recursion *exists*.

Surely it only exists if the type system allows it. After all "polymorphism" does not exist without types, types do not exist like a chair exists, but exist within the context of a theory. Types behave differently depending on the type system (intersection types, vs quantified types). In a strictly monomorphic type system there is no polymorphic recursion. Does polymorphic recursion exist in a rank-1 quantified type system?

If I want to say that the expression of an algorithm seems more natural in a particular type system, is that not a valid comment?

If you want to check whether 'x' is less than 3, you should just check the value in an if statement, not lift it to the type level via polymorphic recursion

That almost sounds like you are confusing the trivial technical example I gave in the other thread with an actual use case. And then extrapolating that all use cases are that contrived.

There are plenty of applications of polymorphic recursion. In particular, any use of non-uniform recursive datatypes (and that includes most interesting GADTs) is impossible without it.

Can you give me a small useful example, that is more elegantly expressed as polymorphic recursion? Just want something that I can add to the test suite for my language, and that might persuade me I am wrong?

Just pick your favourite example of GADTs. For plain datatypes, e.g. Okasaki showed some nifty examples.

I think its better to admit I'm wrong on this one, and look at how I can deal with it. What I would be happy with is some way for the type system to track the dynamic polymorphism. I assume that any type-variables that cannot be assigned ground types will require runtime-polymorphism. What I want to avoid is the programmer accidentally using runtime-polymorphism. I could reject any program that has non-ground types, however, I don't want to reject dynamic polymorphism, only make it a deliberate choice.

Polymorphic recursion requires higher-ranked types, and if I am using first class polymorphism like in Mark P. Jones' FCP, the polymorphic arguments of higher-ranked functions must be given explicit types (in a datatype). As such I could require ungrounded type variables in these explicit types to be marked in some way to indicate they are allowed to be ungrounded, as in:

data Poly = P (a* -> b -> a*)

'b' would have to have a ground type in each application of Poly, but 'a' could be ungrounded.

This is, unfortunately, not true for attribute grammars which are a form of two-level grammars which share some commonality with context sensitive grammars.

Which is why I am a bit stuck, at the moment.

(You can toss analytical information into a parser combinator which corresponds to generating an infinite number of CFG rules. Simplest example is passing a number n for parsing n consecutive productions.)