Lambda the Ultimate

I agree that Haskell has a long history of challenges with instance resolution and partial specialization. We've looked at implicits as well. There are really good insights there, but I don't feel that they provide a full-spectrum solution. I can give challenge examples, but I don't want to hijack the thread.

There are three essential differences:

1. Interfaces provide existential encapsulation of the target object (assuming they have at least one non-static method). Type classes do not.
2. An instance of a type class is a compile-time constant. An instance of an interface is a run-time object.
3. The method table of an interface instance is a compile time constant iff the method binding initializers are constrained to be compile-time evaluable expressions whose outputs are not closed over any mutable. [*] Where this constraint holds, the distinction between interfaces and type classes seems to become blurry.

[*] Strictly speaking, they don't need to be compile-time evaluable. What is necessary is that they be evaluable and idempotent at the first point of use.

My intuitive notion with typeclasses is that if you make polymorphism completely compile time decidable you have probably dropped a fundamental principle that you, in circumstances, just don't want to know at compile time what the specific shape of a value is. It is very probable that you've moved to a very restricted form of polymorphism which makes a number of abstractions you wish for in programming impossible.

For a thought experiment on a functional language with interfaces look here: Hi language. The type checker, especially on interfaces, hasn't been fully thought through and I stopped development on it since I didn't get the performance right. But you can look at the source code and get a feeling how it is to program with interfaces in a functional language. It captures how I think programming should be.

(Oh great. The post calling type classes a compile time feature is gone. Nice going guys.)

If you combine type classes with existential types you get back runtime polymorphism. This gives you control over when runtime polymorphism is used.

If you combine type classes with existential types you get back runtime polymorphism. This gives you control over when runtime polymorphism is used.

I don't get these "runtime polymorphism" and "compile-time polymorphism" labels. Exactly the same amount of type information is available at the point where a type class dictionary is instantiated from a concrete type T, and where an interface is coerced from type T. The only difference is that the coercion also implicitly wraps T in an existential type. I'm not sure why this receives a "runtime" moniker, where type-classes are "compile-time"; dispatch is occurring at runtime in both cases, and both are agnostic to the underlying shape of the type. The existential implicit to interfaces just means interfaces can't support binary methods, but can be packaged together with unrelated T's. I'm not sure runtime and compile-time really captures this distinction.

A type variable must be instantiated to a ground type at compile time, as this is static typing, and otherwise type safety cannot be guaranteed. Existential types are necessary to allow an unknown type to be present at compile time, and they enclose it guaranteeing you can never recover the type enclosed (otherwise it would break type safety). Type classes do not change this they just control static overloading.

That's not quite right. You seem to be assuming that you can always statically monomorphise universal polymorphism, but that is only true if polymorphism is second-class (*). And in that case, it is just as true for existential polymorphism (e.g., some SML compilers "monomorphise" modules routinely).

As soon as you have first-class polymorphism, though (e.g., higher-ranked polymorphic types), you cannot do that anymore, neither for universal nor for existential polymorphism. Furthermore, as naasking pointed out, you can encode existentials with universals then, so there really is no difference in the degree of static knowledge.

In short, the compile time vs run time distinction does not hinge on universal vs existential polymorphism, but on second-class vs first-class polymorphism (and existentials in Haskell happen to be first-class).

(*) And in fact, not even then, as Haskell's counter-example of polymorphic recursion shows -- contrary to popular belief, type class polymorphism is not static in Haskell, not even in plain H'98. Common optimisations notwithstanding.

contrary to popular belief, type class polymorphism is not static in Haskell

Can you provide a reference for this? Specifically where type class instance selection depends on IO? I could not get Haskell to do this, but it was a few years ago, and maybe they have implemented some form of dependant types now?

Here is a simple example:

f :: Eq a => Int -> a -> Bool
f 0 x = x == x
f n x = f (n-1) [x]

main = do n <- getLine; print (f (read n) ())

Note how this has to construct an unbounded number of instance dictionaries.

So type classes aren't a compile time construct which alleviate the need for late binding?

So you construct nested list types effectively "List (List (List ...)))" so presumably the compiler can find the fix point, and its all static. Nothing depends on the recursive type, so it can effectively be ignored? In fact it is existential from the point of view of main - there exists a type 'a' it must have a type (and for each invocation of 'f' it must be a ground type - in this case higher-order unification is finding the fix point) but from outside the function 'f' we cannot find what it is.

However I do concede that it is looking like first class polymorphism might be the thing that is enabling value dependence, but it is existential from a certain point of view.

Edit: for posterity, this is the post where I realised I was wrong. In my defence I don't think Haskell implemented polymorphic recursion when I last looked at this stuff, and I think adding it has changed the type system.

So you construct nested list types effectively "List (List (List ...)))" so presumably the compiler can find the fix point, and its all static. Nothing depends on the recursive type, so it can effectively be ignored?

No, there is no fixed point. For the final comparison to work type-correctly, the program has to construct the specific dictionary eqList (eqList (eqList ... (eqUnit) ...)), with eqList being repeated exactly n times.

I'm sorry, but I don't see what this has to do with either higher-order unification or existential polymorphism.

Looks like Monty Python even influences Haskell design decisions. This is not a larch, not even an almost unbounded list of them.

But seriously. Are dictionaries a runtime construct? If so, this is just an academic manner of blowing up a program through exploiting an (probably unintended) feature of the typing system.

Are dictionaries a runtime construct?

Yes, that was the point of the discussion. ;) And no, this is not unintentional. And more often than not, you can still statically optimise it.

I remembered that. Doesn't seem like they hit the right abstraction though if this is a consequence. But they have every right to explore it, of course.

Ah well. There is stuff I don't understand and then there is stuff I don't even want to understand. The way a number of people reason over types looks like a disaster area to me. It'll probably blow over once.

Call me back when all of you got it figured out. Going to watch a movie now.

Call me back when all of you got it figured out. Going to watch a movie now.

"LOL". This cracked me up. Thanks for the smile :)

I edited my post, I meant first class polymorphism, but wrote the wrong thing. Recursive polymorphism seems to allow runtime dynamic dispatch here, and your right, its not existential.

Okay there's clearly something I am not getting. For example why does this not work:

f :: a -> Int
f () = 0
f [x] = 1 + f x

main = show $ f $ [[[[()]]]]


This does work in OCaml with -rectypes if you change () to [] and you give it the correct type annotation (or let it to be inferred).

This example of yours is horribly mistyped (you can't pattern match on a variable of type a), but I guess your question is more comparing the situation here to what you can do with type classes? Type classes do give some ability to pattern match on types, but it's a completely different mechanism from ordinary pattern matching.

I was comparing to this situation

f :: Eq a => Int -> a -> Bool
f 0 x = x == x
f n x = f (n-1) [x]

main = do n <- getLine; print (f (read n) ())

Where a type is constructed from a value, and so the type is not known statically at compile time (which to me seems like a problem in a static type system). Compared to an example of polymorphic recursion where it is structural recursion on a type known at compile time (which seems fine to me). I guess I should have written:

class F x where
f :: x -> Int

main = print $ f [[[[()]]]]

Edit: One of the follow-up thoughts from the HList paper was that the class and instances for type level functions are very regular and could be automatically generated. So we could allow pattern match over types by lifting to type classes, and this is one of the things I want look at in the language I am working on.

There isn't a type that's being constructed from a value in that example. There is an infinite set of types that f is defined on. The first call to f instantiates f: Int -> () -> Bool, regardless of what the user entered. That function in turn calls f: Int -> [()] -> Bool. etc. Only a finite number of instances are ever demanded (equal in number to what the user enters at the command line EDIT:plus one), but the example is interesting because no finite number of instances is known statically to be sufficient. Thus monomorphic expansion won't work. But every value in sight has a simple type.

There is a kind of container formed though that does reify a value to a type, in that where 'x==x' is I can substitute any type class with functional dependencies or associated types to evaluate type level functions. For example one can define addition on types like this:

class Count x, Count y, Count z => Add x y z | x y -> z where
add :: x -> y -> z

instance Add x y z => Add x [y] [z] where
add x [y] = [add x y]

You can now use the continuation transform (as pointed out elsewhere) to run arbitrary type level computation inside the quantified 'box' created by 'f' (that I was calling existential, and due to the duality of quantifiers appears existential from the outside like a module does, as you cannot find out what the quantified type is from the outside, but you know it does exist, and there is at least one, although as you point out it appears possibly infinite is okay too). So that looks very much like reifying a value to a type to me.

I can effectively implement a type level case statement to switch on this type:

class Case x y | x -> y where
switch :: x -> y

etc...

There's two things I don't like about this, first that it is possible, second that it is only possible inside a continuation. Interesting to note that we wrote about this possibility in the HList paper nearly 10 years ago and tried to make it work, but the compiler failed to compile the code - and I made the mistake of thinking it was a fundamental limitation not an implementation limitation.

Yes, you can use type classes to do type level computation, but there's no way to lift an integer entered at the keyboard at run-time into such a computation.

My problem with this mechanism in Haskell isn't that it's possible, but that it's a horrible Turing tarpit of a language. We should allow arbitrary compile-time execution of code where required.

Also, there's one other distinction to make that I think could help you. I would suggest that we ought to think about type classes as a meta-programming facility for selecting instances rather than as functions or relations on types. Haskell muddies this distinction, but you can see what I mean with extensions enabled (OverlappingInstances, at least), as in the following example:

class Foo a:
  get: a -> Int

instance Foo [a]:
  get xs = 0

instance Foo [Int]:
  get xs = 1

bar :: [a] -> Char
bar xs = get xs 

main = do
   print (bar [0])

What should this print? We call bar with a List of Int. The 'get' function associated to a List of Int, which is the most specific instance, is supposed to return 1. But looking at bar, we see that it's not supposed to know that variable a is an Int. Thus, this code has to print 0 in order to preserve the parametricity property that Andreas mentioned. This example shows that what should be going on with type classes is compile-time instance selection based only on apparent types (to borrow C++ terminology), not some kind of run-time instance selection based on actual types, which to me would be very problematic.

I thought the whole point of type classes was to violate parametricity in a principled way via type-indexed functions. How would you program polytypically/generically without this feature? ie. generic serializers and other generic traversals.

You should write generic traversals like this:

traverse :: Generic a => a -> r

Not like this:

traverse :: a -> r

You can view type classes as violations of parametricity, but I don't like to. I prefer to view them as sugar for inferred dictionary/module passing that's fully parametric.

I thought it was just another means of weaseling out of the expression problem.

I half agree. I want to use types for static resource management at compile time, but I don't want types to depend on runtime values.

I am interested to find where the precise boundary is. I want polymorphic functions for generics and I want something to model interfaces, I am more familiar with type classes, but modules overlap here.

I want to use types for static resource management at compile time, but I don't want types to depend on runtime values.

I don't want types to depend on run-time values, either, so I'm not sure where the half disagreement is. It sounds like there's possibly some disagreement around polymorphic recursion, which I don't (added previous word as an edit) consider problematic.

Yes, you can use type classes to do type level computation, but there's no way to lift an integer entered at the keyboard at run-time into such a computation.

So how would you prevent the value input from the keyboard selecting the type class instance of G (and affecting subsequent type level functions)?

f :: G a => Int -> a -> Int
f 0 x = g x
f n x = f (n-1) [x]
main = do n <- getLine; print (f (read n) ())


I think you may be misunderstanding how that example works (but possibly I'm just misunderstanding your concern). The definition of f is instantiated at a number of types:

f0:: Int -> () -> Int
f1:: Int -> [()] -> Int
f2:: Int -> [[()]] -> Int
...

Here I've given the different instantiations of f different names. Make sure you understand the following: main always calls f0 and doesn't choose which f_n to call based on what the user enters. That is, main doesn't pick the instance of G based on what was entered at the keyboard. Rather, what happens is that f0 calls f1, which calls f2, which calls f3, etc. This call graph is statically known. The only interesting thing about this example is that you can't statically bound how many of these f instances are needed. If the user enters 1000, then you end up calling f1000 before getting to a base case. This means that in a monomorphic expansion of this program, you need infinitely many of these f instances, and so a strategy of complete monomorphic expansion at compile-time fails.

It appears Haskell restricts the application of type classes (with function dependencies?) to the variable at the end of the polymorphic recursion in 'f', so you can do something simple which directly returns a value in that case (count, == etc...) but attempting to use type level computation like 'Add' on this type fails. For example using the earlier definitions of Count and Add, and a modified version of 'f' using continuation passing:

#!/usr/bin/env runhaskell -XRankNTypes -XMultiParamTypeClasses
-XFunctionalDependencies -XFlexibleInstances -XFlexibleInstances -XUndecidableInstances

class Count a where count :: a -> Int
instance Count () where count () = 0
instance Count a => Count [a] where count [x] = 1 + count x

class (Count x, Count y, Count z) => Add x y z | x y -> z where add :: x -> y -> z
instance Count x => Add x () x where add x () = x
instance Add x y z => Add x [y] [z] where add x [y] = [add x y]

f1 :: Count a => Int -> a -> (forall b . Count b => b -> r) -> r
f1 0 x = \k -> k x
f1 n x = \k -> f1 (n-1) [x] k

{-
f2 :: Add a a b => Int -> a -> (forall a . (Add a a b) => a -> r) -> r
f2 0 x = \k -> k x
f2 n x = \k -> f2 (n-1) [x] $ k
-}

print_n x = print $ count $ x
print_double_n x = print $ count $ add x x

main = let x = [[()]] in do
    print_n x
    print_double_n x
    f1 2 () print_n
    --f2 2 () print_double_n
    n <- getLine; f1 (read n) () print_n
    --n <- getLine; f (read n) () print_double_n

The version using Count in the polymorphic recursion works, but trying to use Add fails. It fails for both the version where the number is known at compile time and where it is not known until runtime.

- Why does the 'Count' version succeed when it appears it should not?
- Why does the 'Add' version fail when the number is known statically at compile time?
- This all appears very arbitrary from the type system point of view. Are these restrictions implementation dependent? I don't see a fundamental reason why these should fail looking purely at the type system and treating the type-classes as constraints on types. Is it that the constraints are unsolvable, or that Haskell is trying to restrict things to the implementation?

You're losing me. Why do you say that the Count version shouldn't succeed? That looks fine to me. You're building up a Count instance on the way down a recursion and are then deconstructing it at the bottom of the recursion.

But then I'm unsure how f2 is supposed to work. Did you intend for it to call f1 like it does instead of recursively calling f2? It looks like that makes it so that only a trivial Add () () () instance will be created in your call to f2. Assuming that was supposed to be a call to f2, I'm not sure how it's supposed to solve the constraints need to make that recursive call. We have an instance Add a a b, and we want Add [a] [a] c. Looking at the instances available, it will create that instance by introducing Add [a] a d, with d = [c]. Now what? You don't seem to have a rule that matches this form, so aren't we stuck?

I don't have ghc installed on this machine, so I can't play with this.

The larger issue is that I don't see where you're going with any of this. Is your goal complete monomorphic expansion of the program?

My goal is to understand what is going on. Yes, you spotted the deliberate mistake, but fixing it does not change the fact it does not work. The cases for Add should work as far as I understand it, and it works for all the test cases when the types are statically known like add () [[()]] etc.

Add has a functional dependency, so in Add a a b, the first two arguments together uniquely determine the third, so you can see this as a type level function where the type of 'b' is an output form Add not an input. For example:

Count a => a -> Int

If this works, then so should this (where Add has the fundep, Add x y z | x y -> z)

(Add a a b, Count b) => a -> Int

As b is uniquely determined by a, if we know the type of a, we know the type of b. So 'Add a a b' should work everywhere 'Count a' did.

I think the problem is that you're looking at the type class mechanism as extracting information from types globally instead of thinking about local inference. The point of one of my earlier posts was that it doesn't/shouldn't work that way -- the fact that there is an instance for the actual types that will eventually be present at run-time doesn't help the compiler produce an instance based only on the apparent types in a polymorphic function. Let's simplify your example down to just the code that builds the instance (eliminating the continuation/instance deconstruction stuff):

f2 :: Add a a b => Int -> a -> Int
f2 0 x = 0
f2 n x = f2 (n-1) [x]

Even this won't work. We're in a context with (Add a a b), x::a, and we're trying to call f2 recursively. So we generate fresh variables for the recursive call f2 :: Add c c d => Int -> c -> Int. The first argument, n-1, is an Int, so that checks out. The second argument is of type [a], so we set c = [a] and try to find an instance of Add c c d = Add [a] [a] d. There's only one rule that matches: Add [a] [a] d = Add e [f] [g]. So we set e = [a], f=a, d = [g]. But that rule required (Add e f g), so now we're looking for (Add [a] a g), and that rule matches nothing so we're stuck. We emit an error message. (Disclaimer: I haven't tried this)

The compiler does not do a global program analysis to decide that all of the types ever used here are of the form [[...()...]] and then somehow reason out which instance to use and it doesn't do instance selection at run-time with the "actual type".

How about this then:

f3 :: Add a b c => a -> b -> Int
f3 x y = count $ add x y

main = do print $ f3 [[()]] [()]

Which you can use fine. It seems to do 'whole program' analysis and the HList library relies on this kind of type level computation. It works fine not matter how many levels deep the 'add' is put, and across module boundaries. The only time it does not work is inside a polymorphic recursion. I am trying to understand if this is a limitation of the implementation or the type system.
It think we are kind of agreeing anyway, as I agree it does not do instance selection at run time with the 'actual' type - but in that case why does 'Count' work where it appears to be selecting instances at run-time after I input the number?

I don't see that as whole program analysis, unless you mean all instances are considered. The choice of an instance for Add a b c is made at the call site to f3. I'd expect you can get the problem of the previous example without recursion:

f1 :: Add a a b => Int -> a -> Int
f1 _ _ = 0

f2 :: Add a a b => Int -> a -> Int
f2 0 x = 0
f2 n x = f1 (n-1) [x]

I think this will complain at the call to f1. The problem is that the rules you laid down for Add don't cover this context.

How type classes work across modules in Haskel is something I know nothing about, so I won't comment.

No, I mean it analyses all the types in the program, and makes instance decisions based on any types that are known statically at compile time. This works:

f1 (0 :: Int) x = count $ add x x

f2 (0 :: Int) x = 0
f2 n x = f1 (n - 1) [x]

So just leave it to type inference and it works. The inferred types turn out to be:

f1 :: Add y y a1 => Int -> y -> Int
f2 :: Add t t a, Add [t] t z => Int -> t -> Int

Of course type inference does not work on polymorphic recursion, so maybe the limitations for this are the same as for type inference?

Well, instance selection is still local in your example. I'm sure it is true that the inferred types around polymorphic recursion won't be as tight as they will with polymorphism used in a DAG.

I don't think I understand what you mean by local then. Type inference works over the whole program and will infer the types for uses of polymorphic functions, which implies the instance selection.

So the propagation of types trough the program is 'whole program analysis'. Header files are used to write the inferred types in separate compilation, so the compiler can read them in when using the object file in further compilation.

Type inference is a local process: a type is assigned to each function based only the constraints found in the body of the function. Instance selection happens at the same scope. Constraints in those local contexts are solved by inserting new instances based only on the local context.

But doesn't that include reference to a mono-morphic and poly-morphic environment that bring all sorts of (global) definitions into that local context?

Yes, but I call that local. What kind of analysis can you do if you aren't allowed to use summary information (like types) of names referenced in the environment? Or do you consider all analyses global?

It sounds like we both have the same understanding of what is going on but want to name it differently. I want to call it global because you need access to a global polymorphic environment to infer and check types.

Perhaps we can agree to call it "local analysis with a global polymorphic environment"?

I'll just call it local analysis. ;) But I understand what you mean though and don't to argue definitions.

Let us know when your language project becomes available for review.

In short, the compile time vs run time distinction does not hinge on universal vs existential polymorphism, but on second-class vs first-class polymorphism (and existentials in Haskell happen to be first-class).

That's an excellent summary. I was struggling to explain my more informal understanding of this, but that hits the nail squarely on the head.

Yes, I think I can agree to that, however it behaves like an existential, the run-time types have to remain in the box. It is existential from the outside and universal from the inside (a bit like modules?)

So I was right, I was just looking at things from the outside, where they look existential.

Edit: I am not so sure this is the right distinction now, I can see plenty of examples of polymorphic recursion and first-class-polymorphism that are safe to use with static dispatch.

Exactly the same amount of type information is available at the point where a type class dictionary is instantiated from a concrete type T, and where an interface is coerced from type T.

A type must always be concrete in a static type system. You cannot have an unknown type or the program will not pass type checking. Can you give me an example where you don't know the type at compile time?

A type must always be concrete in a static type system. You cannot have an unknown type or the program will not pass type checking. Can you give me an example where you don't know the type at compile time?

Polymorphic parameters aren't concrete. If a polymorphic parameter also has a type class constraint, there you have your runtime dispatch on a non-concrete type (I'm assuming "concrete" to imply "monomorphic" obviously). The step to interfaces is simply making that parameter existentially quantified (Edit: I don't see how this adds any more of a "runtime" quality than was already there, however).

Well they are concrete when you use the function, you have to consider the whole program. Where do you apply a polymorphic function to a type you do not know at compile time?

Well they are concrete when you use the function, you have to consider the whole program.

If you're considering the whole program then the same argument applies to interfaces. You can defunctionalize interface dispatch, and your runtime polymorphism goes out the window in the presence of whole program compilation.

Where do you apply a polymorphic function to a type you do not know at compile time?

Within another polymorphic function (like Haskell's sortBy), or in a separately compiled library. I'd be surprised if you've never called a function from within a polymorphic function (like a map within a fold).

This is all happening at compile time. Something has to call the fold which contains a map. Can you give me an example of some code you think the compiler cannot resolve to concrete types at compile time? If types only depend on other types the compiler can determine everything at compile time - this is a fundamental property of static type systems. Yes the implementation may be doing stuff with shared function implementations and boxed values - but the type system stops anything from happening which is not type safe. The only way a type is 'runtime' is if it depends on a value. So consider a function that inputs a value from the user and returns a Float if the value is 1 and an Int if the value is 2. How would you do that?

Every case where the types do not depend on values really can be determined statically at compile time. The type system considers all the types in the module headers and every type in the whole program must be grounded for compilation to succeed (ignoring existentials).

This is all happening at compile time. Something has to call the fold which contains a map. Can you give me an example of some code you think the compiler cannot resolve to concrete types at compile time?

I already specified an example of function: Haskell's sortBy in the standard prelude. All such polymorphic functions have unknown concrete types when they are compiled.

And if you consider consider polymorphic types to be concrete types at "compile-time", that's fine, but then so are existential types which are the only distinguishing feature of interfaces in so-called "runtime polymorphism", and once again there is no distinction.

I'm afraid you will have to explain precisely what you mean by "compile-time".

We need to not confuse the implementation with the semantics. When sortBy is compiled separately a header file is created in an internal compiler language. This file contains the necessary information to elaborate the function. Elaboration is taking a function template with type arguments and creating executable code by substituting those arguments at compile time. Now implementations may choose to use boxed types and share functions, but they semantically behave as if elaboration were taking place.

The only way to have a type that is truly unknown at compile time is to have a type depend on a value that comes from IO (reading a file, keyboard input, network packet, channel from another program etc). In order to deal with this you need to use an existential type. (edit: if you insist on returning different types - obviously if you don't need something that is 'open' then a plain-old-datatype would be simpler - open-datatypes are a nice alternative to all this type-system mechanics, but of course you need open-functions too).

Consider the classic 'Shape' example - where you have an interface for drawing shapes, and then objects that implement that interface called 'Circle', 'Square' etc. If you want to allow the user to pick shapes from a palette and draw them, and you use a type-class for Shape, with datatypes for Circle and Square, how would you return the shape the user selected from a function?

Now implementations may choose to use boxed types and share functions, but they semantically behave as if elaboration were taking place.

Your elaboration argument seems like a red herring. The semantics of a polymorphic parameter are that it's concrete/monotype is unknown when the function definition is compiled, and that's what matters. That you can specialize it later when more type information is available is irrelevant. You can do the same with interface method dispatches when the type information is available (via a defunctionalization transform, like I've mentioned).

Furthermore, the universal quantification of polymorphic parameters and existentials are formally duals. A rank-2 universal is an existential. Why does adding a rank suddenly move something from "compile-time" to "runtime"? Is a rank-3 universal "future-time"? This distinction doesn't seem to make sense. Rather, both universal and existential parameters are "runtime" parameters, just with different properties.

The only way to have a type that is truly unknown at compile time is to have a type depend on a value that comes from IO (reading a file, keyboard input, network packet, channel from another program etc). In order to deal with this you need to use an existential type.

No, you can defunctionalize if the set of all inputs are known, or you can use HLists, again exploiting runtime parametric polymorphism, if the set of possibilities is itself generated from some input.

Existentials merely allow one way to modularly extend the set of data types that may participate in this sort of runtime negotiation at runtime, but they aren't essential to the negotiation.

As one of the authors of HLists, I think you will find the polymorphism is static. HLists uses type indexed types, so it is a kind of type union, where you know all the possible types at compile time. Note the fact that it is type-indexed is what makes it possible for the compiler to know the type being extracted at compile time. You will still not be able to put a different type in which is dependant on user input though as reifying a value not known at compile time to a type is not possible without dependent types. You can reify constants known at compile time, and the compiler can aggressively do partial evaluation to evaluate functions whose inputs are all known at compile time, but thats it.

I don't see how defunctionalization helps, perhaps an example where defunctionalization enables a different type class instance to be selected based on input from the user?

Perhaps it is better to focus on 'runtime' which is clearly after an executable has been generated, to avoid confusion with the implementation of a particular version of a language. For example Haskell could be implemented by elaboration using unboxed types and whole program compilation, the fact that GHC uses boxing to enable separate compilation and function code sharing is an implementation detail. The elaboration argument is not a red herring, and is in fact fundamental. It is why dependant types cannot be implemented without staged compilation or dynamic code generation.

For the quantification, the dualism is precisely why what I am saying is true. When inside the box 'x' is polymorphic and stands for any type (maybe no type exists), when outside the box (forall x . x) x is existential and requires a witness type, it is true for some _at_least_one_ type, you must provide a concrete witness type to prove this is true. The compiler has to close the box and provide the witnesses for the program to pass type checking. Because x represents a single term, it must take precisely one type. Type safety is based on this, the program is proved safe because exactly one witness type exists for every type variable. (no more than one or it is ambiguous, and Haskell uses defaulting tricks to avoid this with numeric literals for example).

If you have the whole program then you can eliminate existentials by code duplication just like you can eliminate universals by code duplication as you suggest. It's just that in one case you have to duplicate the continuation and in the other case you have to duplicate the expression itself.

For instance consider a function foo : Show a => T. As you suggest you can elaborate that to one different foo for each type: foo_int : T, foo_string : T etc. Note however that this breaks down if you have polymorphic recursion because you may need an infinite number of elaborations. If you have higher rank types you can still do this but you will need some type tags that you dispatch on at run time.

The same thing applies to existentials. If you convert the program to continuation passing style, then at every point where you have the construction of an existential package with type t and value x, you can convert it to have a continuation of type (forall t. x -> a) -> a. This way you eliminate all existentials and you're left with only universals. Now you can apply the same code duplication to eliminate them. In general you will end up with higher rank universals so you will get those type tags after the transformation.

However you can define notion of existentials that can be eliminated at compile time that is just like the class of universals that can be eliminated at compile time (i.e. rank-1 without polymorphic recursion). If an existential is only ever directly unpacked and not passed on to arbitrary places, then you can eliminate them just like you can eliminate universals that are only ever directly applied and not passed on to arbitrary places (like for example in ML where you cannot pass a polymorphic function to another function, the type parameter is always directly applied).

Summary: the distinction between static and dynamic or compile time and run time is not between universals and exisentials. In fact they are symmetrical. The thing that matters for whether you can eliminate the dispatch statically is restrictions for how those universals and existentials are used in the program.

you can convert it to have a continuation of type (forall t. x -> a) -> a

The continuation passing transformation is doing something else here and changing the meaning with respect to the quantifiers. There is a fundamental asymmetry that does not happen with 'non-existential' types, you can push things into the box with a continuation passing transform, but you cannot pull stuff out.

I don't think you can eliminate existentials at compile time. For example:

data Box a = forall a . Showable a => Box {unbox :: a}
let l = [Box 'a', Box "b", Box 1, Box True, Box 1.0]
do {x <- getLine; return $ case (l !! read x) of (Box y) -> show y}

This shows type-class selection based on a type at runtime. But note the type must remain inside the existential box so:

do {x <- getLine; return $ show $ unbox $ l !! read x}

Is not allowed due to the type variable escaping the existential box. However we can push polymorphic functions into the box:

(\(j :: forall a . a -> a) -> do {x show $ j y}}) id

But we cannot push any function in that uses a type class not declared on the original existential box:

(\j :: forall a . Num a => a -> a) -> do {x show $ j y}}) (\x -> x + 1)

Right, that's an example where you cannot eliminate the run time dispatch. However as I tried to explain it is not just existentials that have this property, universals have this as well. You could write it in terms of universals like this:

type BoxConsumer r = forall a. Showable a => a -> r
type Box = forall r. BoxConsumer r -> r

to create a Box x you do this:

mkbox : Showable a => a -> Box
mkbox x = (\boxconsumer -> boxconsumer x)

and to unpack a box case box of (Box x) -> ... you do:

box (\x -> ...)

So we've encoded that example with universals only. So it cannot be simultaneously true that universals result in 'static' or 'compile time' dispatch and existential are 'dynamic' or 'run time' dispatch, regardless of what the notion of compile time and run time is. Therefore, whether the dispatch can be done statically depends not on whether we're using existentials or universals, but on how those are used.

What naasking was saying at the start of this thread is that with type classes and interfaces, the type dispatch happens at the same place. In your example the type dispatch is happening in this line:

let l = [Box 'a', Box "b", Box 1, Box True, Box 1.0]

The compiler inserts a type class dictionary as an additional argument to the Box constructor. So here too the type dispatch is happening statically in a sense. This is the same as what's happening with interfaces in object oriented languages (or at least what could be happening, actual implementations may differ). At the place where a concrete object type is cast to an interface type, the compiler inserts the 'interface dictionary' aka vtable to be packed up with the object. I believe that this is how Go implements interfaces (?). However in both cases the actual dispatch is happening because this code:

case (l !! read x) of (Box y) -> show y

is translated to something like this:

case (l !! read x) of (Box y showfn) -> showfn y

so the run time dispatch is happening because there is a dynamic function shownfn that is extracted from the box.

Andreas and Jules have better explained what I would have said here, but I'll just expand a bit on what I was thinking re:HList.

HLists uses type indexed types, so it is a kind of type union, where you know all the possible types at compile time. Note the fact that it is type-indexed is what makes it possible for the compiler to know the type being extracted at compile time.

As Jules explained, converting an existential to a universal consists in converting to continuation passing style. When specifying HList in my previous comment, I was considering something like the following for when dynamic loading is needed to dynamically extend the list of possible types:

class ExpectedClass a where
  ...

withModule :: forall a b. a -> (forall m. ExpectedClass m => a -> m -> b) -> b

So the program would be structured in a continuation passing style with a set of nested withModule loads to build a dynamic HList. There are no existentials in this program.

See my example above, yes you can push polymorphic functions, constrained by the type classes known at compile time into the existential box.

Okay, so I have worked out where the issue is. First class polymorphism enables higher-order types. From outside the quantifier these all look existential, in that run-time types cannot escape the 'box' created by the quantifier, hence why I was referring to them as existential. From the inside they appear universally quantified.

But what to do about the list selection. You can't put the world inside the box can you?

You don't need to "put the world inside a box" (if I guess correctly what you mean by that). Existentials can be fully encoded as universals (this is standard). Translate the type

data T = forall a. C a => T (Whatever a)

to

type T = forall b. (forall a. C a => Whatever a -> b) -> b

and the expressions

T e
case e of T x -> e'

to

\(f :: forall a. C a => Whatever a -> b) -> f e
e (\x -> e')

respectively (similarly for a 'let' instead of 'case'). GHC may force you to throw in some extra type annotations. Example: Simluate

data Showable = forall a. Show a => Showable a
xs = [Showable "abc", Showable 1]  -- xs :: [Showable]
ys = map (\(Showable x) -> length (show x)) xs

with

type ShowableCont b = forall a. Show a => a -> b  -- for convenience
type Showable = forall b. ShowableCont b -> b
xs = [\(f :: ShowableCont b) -> f "abc", \(f :: ShowableCont b) -> f 1]  -- xs :: [Showable]
ys = map (\(e :: ShowableCont Int -> Int) -> e (\x -> length (show x))) xs

Run with -XRankNTypes -XScopedTypeVariables.

So having got a bit further in understanding where the limits of static dispatch are, what do I need to do if I want to limit something like type-classes (modules/interfaces) to static dispatch in the type system.

The polymorphic recursion example seems particularly problematic. Would you need to exclude first class polymorphism and polymorphic recursion? Many uses of first class polymorphism seem safe, for example passing a polymorphic identity function.

If I wanted to enforce static dispatch, so that I can use unboxed types and specialised functions, do I just need to ensure that all type variables have a ground type at compile time? I can still allow first class polymorphism, but probably not polymorphic recursion, again some forms of polymorphic recursion seem safe, the equivalent of structural recursion rather than general recursion, that is polymorphic recursion controlled by types not values.

If you allow polymorphic recursion, you can't specialize functions. You can still use unboxed values by passing the representation of the type at run time. If you allow first class polymorphism, you would need to do some kind of flow analysis to determine the set of possible types at each type variable. Even then you would still need to pass around run time type tags and dispatch on those to select the correct code, this is simply unavoidable. For instance consider the Box type elsewhere in the thread. If you want to use unboxed values then a Box of int and a Box of double have different size. So you would need to attach some kind of run time information to a box to indicate its size.

Okay so polymorphic recursion is the problem (for me). I'm pretty sure this is something ghc did not support last time I looked at this, so a possible excuse for my ignorance.

My first thoughts are restricting the introduction of type variables is enough. For example forall a . a -> a is fine but forall a b . a -> b is not, because without polymorphic recursion you can't introduce a type unknown at compile time. It occurs to me that the type signature of the polymorphic recursion example elsewhere has the same problem forall a . Int -> a -> Bool.

My intuition would be restricting quantified variables in first class polymorphic types and polymorphic recursion to not be only on the right hand side of an arrow is enough.

Anyone have any ideas if this restriction is sufficient? If there is a less restrictive option?

Polymorphic recursion has been an official part of the language (and implemented by all compilers, AFAICT) since the dawn of Haskell.

The property you seem to be after is parametricity. You cannot achieve it by any form of restriction on type variables. What (seemingly, not actually) breaks parametricity in Haskell is the presence of type class constraints, so you would have to drop those.

There is no excuse for my ignorance then. Oh well. I am pretty sure we tried reifying types and failed, but maybe the mistake was to try using type classes.

Anyway I disagree with type classes being the problem as type level computation is essential to what I am trying to do, and there are many safe uses.

Polymorphic recursion does seem to be the problem as far as I can see at the moment. Is there a safe (ie all types known at compile time) use for PR.

Polymorphic recursion does seem to be the problem as far as I can see at the moment. Is there a safe (ie all types known at compile time) use for PR.

The first motivating example I saw was in the book "Purely Functional Data Structures" where polymorphic recursion was used to control the shape of a growing tree at each level.

I've been working on a compiler (stuck inside a corporate box, so never to be made public sadly) that makes a lot of the same observations I've seen you make in this thread (and the other one). Basically, if you interpret type classes (and qualified types in general) as constraints guiding monomorphization, you can straightforwardly generate very good code.

Maybe we could compare notes offline.

Edit: I see that I ignored your qualification that the types be known at compile-time. I haven't seen a useful case of polymorphic recursion where types are known fully at compile-time, except maybe I guess if you fully constructed such a balanced tree (as mentioned earlier) at some point, and just needed to deconstruct it.

I want to reply separately to this, as its a different point to the other about restricting first class polymorphism and polymorphic recursion.

I am intending to not use any run time type information, but there will be complex issues to resolve. First is no garbage collection achieved through stack allocation and function objects for closures. The basic types will be the machine primitive types (C--), and product types will basically be c structs. Values returned from functions using move semantics. Sum types tagged unions. The size of any data type is the size of the biggest product type in the sum, which can be determined at compile time and copy, allocate and delete specialised accordingly. This is why I need the type system to prevent any types depending on run-time values.

I would appreciate any thoughts about anything I may have forgotten.

Flattening sum types does not work, unless you forbid recursive types. For the same reason, you cannot flatten closures, unless you disallow closing over functions, which makes closures rather useless. Moreover, what would be the size of a closure object anyway?

Also, you cannot have move semantics for closures when you want to be able to close over mutable variables, which could be shared by other closures.

Generally, neither closures nor other recursive constructions work without heap allocation (and thus GC). (Related question)

Furthermore, not using GC dose not actually buy you that much for unboxed values either. What GC needs to know is how to traverse each value. So you have to keep some kind of metadata yes. But you already have to keep *some* metadata, the size of the value, to be able to pass the values around. For example think about a polymorphic identity function, at the machine code level it has to do something genuinely different for different sized values.

So what you can do is instead of removing type variables at run time, you convert them to normal value level parameters and pass around a representation of types in them. This allows you to keep the values themselves unboxed. This is quite different than the tagging many implementation are doing. They attach a type tag to each value. For instance if you have a list of doubles, each element is stored by a pointer to a piece of memory that has a type tag and a payload double value. This is quite wasteful because we are storing the same type tag in every single element of the list. The metadata representation at run time does not exactly match the type structure.

With the representation where you pass around type parameters at run time, you store the type structure List Double once, and then the actual list is stored as a list of unboxed doubles without any type tags.

I don't know what the performance of such a scheme would be, but I expect that passing around the type structure would have little overhead since those structures are small and because they flow independently of values existing optimization techniques would be quite effective to reduce their overhead. If you want to go for maximum performance you could even allow staging annotations on type variables to do controlled monomorphization.

Maybe saying no garbage collection is wrong, as I will use reference counted pointers. We would statically know the size of the thing pointed to and can deallocate when the last pointer is dropped. I realise reference counting is a form of GC, so perhaps no GC is too strong a statement. No runtime is probably a better way to say it. In many cases local variables will not leak from functions and can be stack allocated. The only time heap allocation is needed is when a function is returned from another function, passing and returning data does not need heap allocation. I will mostly use something like RAII from C++, so a handle for an object will be stack allocated, and the memory (for say an array) would be heap allocated. When the handle goes out of scope the memory will be deallocated. Static analysis will track when variable capture occurs and the variable will be heap allocated with a shared pointer instead. Each shared pointer will be stack allocated, so when the last shared pointers destructor is called the heap memory will be freed.

Consider the following made up syntax:

fn = {
(inj, prj) = {
var x
var y
return ({\z . x = z}, {return x})
}
inj 3
print pro
}

inj and prj are stack variables (in fn stack frame), y and z are stack variables in anonymous functions, only x need be on the heap and would use a shared pointer, this would be inside each function object. The two function objects would have their handle returned by move semantics so the handle is in 'inj' and 'prj' stack variables respectively.

There are a few more subtleties, like the stacked handle is not the 'value' that is passed about, that is a plain pointer with no ownership as long as we are inside the scope. Static analysis determines if variables ever escape scope and when to transfer ownership to a shared pointer.

Edit: so its probably easier just to say I am using shared pointers for GC, plus some optimisation techniques using memory regions.

The only argument for reference counting vs a proper GC is simplicity of implementation.

Scripted languages can usually deal with the associated cost of updates on the counter since they usually marginally touch the memory w.r.t. compiled languages. You can just push a large number of operations to the runtime, vannila C, do a lot of work there, and forget about the updates (you'ld normally need in a compiled language) until you return from all the work. It also helps in keeping the space consumption down; in essence, you're just using the C GC.

It isn't a bad choice, but for compiled languages which deal with a large number of objects it's usually a poor choice. (Though some people sometimes revert back to reference counting in elaborate schemes to get a bit more performance out of a tracing collector.)

Mainly for performance. By supporting say a mutable array using memory regions (like a C++ vector), where the values are unboxed and the type carries all the information necessary, like a matrix with phantom types for the rows and columns, the handle will be stack allocated in the outer context, passed by plain pointer into functions that use it. Return values will be created before the function call, and the results written directly back (as if passing the pointer in). So a function like:

add :: Matrix 3 3 -> Matrix 3 3 -> Matrix 3 3

would get passed two pointers to consts and one mutable pointer (reference).

The point is to allow very high performance inside the stack frame where the region is held.

I might make the shared pointers explicit, and just have the type system / static analysis throw an error if you leak a variable. This would require you to declare the variable as 'imported' inside the a function that gets returned out of the definition scope. This would be inline with the general design concept of making the programmer explicitly ask for anything that compromises performance.

Doesn't look like a valuable idea. Memory regions are usually avoided because regions which reference each other can easily lead to space explosions or a lot of copying between the regions.

If it would be a sensible idea you'ld find a lot more people doing this.

If your goal is to write a language then do what everybody else does and just copy the OCaml runtime and concentrate on the language. You'ld just get a stack and automatically garbage collected heap for free.

I wanted to experiment with a few basic ideas so I ended up with GC on a DAG (not a stack or a general graph, in essence) which I implemented with a straightforward stop and copy algorithm for general graphs. (I experimented a bit with GC on DAGs but stop and copy is hard to beat.) The performance is good but the bootstrap compiler was too slow.

The last thing a Jedi must do before he is a master it to build his own lightsabre. Substitute programmer for Jedi and programming language for lightsabre.
Besides I have been cultivating a good beard, which ensures my success.
If everyone were doing it I would not need to, I could just use theirs.

Enough bad jokes, I do have some motivating examples.

Sorry man, but this has been tried by too many people and they all end up with a semi-unusable language. Though they are sometimes interesting.

We know stack based languages are Turing complete. But try some thought experiments with some list processing functions where the lists are allocated on the stack and you'll quickly find that a large number of those functions simply aren't expressible, or would need to retain the original value on the stack indefinitely.

You don't have time for this. In general, if you're developing a language, you've got just enough time to write an interpreter over an (untyped) language with a GC collected heap. That also will mostly do and have reasonable runtime performance. Anything extra, moving stuff to a stack, unboxing values, elaborate typing, compiling, other stuff, just takes years to get right.

There may not be primitive lists, but if there were they would be managed by a memory region whose handle is held on the stack. When the stack handle goes out of scope, the memory region is free along with its contents. So the list would be in the heap, but controlled by the stack (owned by the handle). A bit more detail is in the post above.

And a myriad of other scripting/semi-compiled languages.

Quite the opposite, this is compiled and has no runtime.

People here seem to be a bit restricted in their interpretation of types and values. Too much Haskell maybe?

A list of shapes where you can ask each shape, triangle, box, circle, what their surface area is, is in many languages (even functional ones like OCaml) a normal expressible thing. If you cannot do this in, for example, Haskell you might wonder whether that language dropped an expressive construct necessary for programming.

(If so, I imagine the rationale for not having this kind of abstraction is runtime overhead. It used to be a slow language, in some perspectives probably still is.)

No idea what some of the other discussions are about.

What question are you answering?

I (obviously :) ) second ML modules. A quick list of its highlights:

• Fully typed: every module has an inherent "type", namely its interface (known as a signature).
• Structural many-to-many subtyping relation between interfaces (interface inheritance): every signature can have arbitrary many subtypes (extensions or refinements) and many possible supertypes (restrictions or generalisations). Subtyping is fully structural, i.e., need not be declared explicitly.
• Structural many-to-many "matching" relation between modules and interfaces: every module can match many signatures, and every signature can be matched by many modules. Matching is also structural, i.e., modules can match all supertypes of their implicit "principal" signature, without the need to declare them.
• Many-to-many inclusion relation between modules (implementation inheritence): a module can be defined to include arbitrary many other modules, and be included in arbitrary many other modules. (However, no OO-style overriding: included members can be shadowed, but not changed.)
• Structural parameterisation over modules: a module can be a so-called "functor", a function from arbitrary modules to arbitrary modules. Functor application can be interpreted as instantiation or linking.
• Compositional language: the module system is closed under nesting and abstraction, i.e., a module can contain any entity of the language (including arbitrary other modules) and be parameterised over any entity of the language. In other words, modules and signatures are hierarchical and functors are higher-order, i.e., they can be parameterised by (or return) other functors. The module system essentially is a (terminating) typed functional language on its own.
• Formally sound system: there is a well-developed theory for the semantics of ML modules, including formal results about all important properties.

Of course, there are downsides as well:

• Modules are rather verbose. In particular, all parameterised modules must be instantiated explicitly, and the parameters must be provided explicitly (unlike type class instances).
• By default, modules (unlike objects, but like type classes) are second-class citizens. While they can be packaged up as first-class values, doing so again is rather verbose. Parameterising over a module typically requires writing a functor instead of a function.
• Most variants do not support recursion between modules, or only limited notions of recursion.

Oops, this got longer than planned...

I like modules (even Ada ones) more than the object oriented approach. What I don't like is the special syntax / language outside of the main language. A simple solution is records-with-associated-types, which unify records and modules into a single first-class entity, so functors become ordinary functions. They should have all the advantages listed above, and remove two of the listed disadvantages. You can also combine this with instance-arguments to allow implicit selection (as in type classes) and explicit (as in modules) where you want it. So Records, Modules and Type-Classes can all be rolled up into one first class entity, overcoming the dis-advantages of modules at the same time.

I don't know if any languages out there already do this, I would be interested to see examples of this approach, as I am working on a little language using this approach.

Well, one of the fundamental results of the module literature is that you can have either first-class modules (along the lines you sketch) or a decidable type system, but not both. Also, you typically want some amount of type inference in the core language, which is not much of an option for modules. How to get a better compromise between expressiveness and convenience is still more or less an open problem.

Isn't it better to have an undecidable static computation - i.e. when the programmer is around to evaluate and debug - than an undecidable runtime computation? Why is it we oft accept the latter but not the former? Is it a form of hypocrisy?

It seems to me that a Turing powerful language to express modules and compile-time behavior is not a bad thing... assuming, of course, that we can reason about, control, and debug compile-time performance and behavior without more difficulty than we today reason about, control, and debug run-time performance and behavior.

I actually agree that undecidable type checking is not necessarily a show-stopper -- it depends on what kind of environments the language is supposed to be used in. Though it is worth noting that it leads to a drastically more complicated semantic model, and some forms of formal reasoning about programs might become next to impossible. From the immediate practical perspective, however, type inference is the more serious problem. For me at least, a language without some degree of that is not worth considering.

drastically more complicated semantic model

People who say this tend to follow it by pointing to a semantic model with multiple layers: one for the runtime (e.g. value-level lambdas), and another semantic model for the compile-time (e.g. type-level lambdas), and a formal description of how these relate. OTOH, if we accept an undecidable compile-time computation, then I think we don't need a separate semantics from the runtime. One level of lambdas will do. Of course, we do need some way to express and enforce staging. But it can be expressed and enforced the same as we might express and enforce staging at runtime - e.g. by use of arrows and applicatives, algebraic effect, or capability security.

Is the latter option truly "drastically more complicated" than the former? I haven't seen convincing evidence of this complication.

Regarding type inference, I don't believe Turing completeness has ever really been the showstopper there. The type-inferred languages I've used (ML, Haskell) are Turing complete, for example. Even a fair portion of dependent types can be inferred. I suppose if you use type-driven dispatch (e.g. using typeclasses) then this would complicate inference. But we might instead use more dynamic language idioms, e.g. modeling CLOS multi-methods, to explicitly compute dispatch at compile time. (See my earlier comment.)

It seems to me that many 'drastic complications' will evaporate if we're simply willing to seek a new ways to solve old problems. And the resulting system will be simpler... or at least more explicit and controllable.

I don't know how you'd build a relational model for a language without a terminating type system. Without such a model, you cannot apply most of the existing relational reasoning techniques, and thus will have a hard time proving any form of interesting program equivalence or abstraction property, for example.

As for type inference, that is unrelated to undecidability (this may have been unclear the way I wrote it). Even for a decidable version of modules, most type inference is pretty much out the window. Maybe you can get partial inference covering most of the subset of modules that doesn't actually use any of the power of modules, but so far, nobody has come up with such a system (although I have some vague ideas).

hard time proving any form of interesting program equivalence or abstraction property

It is not clear to me what you mean by a relational model for a language.

But I think we don't need a "terminating type system" to reason about a broad variety of equivalence properties. For example, we don't need to know the full type of `foo` or `baz` to know that `baz (foo x) (foo x)` is equivalent to `let r = foo x in baz r r`. It is my impression, even, that this is the common case: most useful equivalencies (by which I mean: equivalencies developers and optimizers can effectively use, e.g. to refactor or optimize code) are expressed structurally and enforced by construction, and are thus orthogonal to type checking. At least, I don't recall ever encountering any counter-examples. Do you have one?

Even for a decidable version of modules, most type inference is pretty much out the window.

Is it really? I don't see any particular problem with it. I wonder what additional assumptions you're making that I'm not, e.g. regarding separate compilation, effects model, subtyping, and type-driven dispatch (typeful overloading).

Relational model in the sense of logical relations, see e.g. the classic papers by Reynolds about relational parametricity, or by Mitchell about representation independence. Or if you don't mind another plug, our POPL'09 paper about representation independence for stateful ADTs, for just one pointer, since that contains a little list of -- you would think -- fairly trivial examples.

More generally, most program properties or equivalences that involve types in an interesting way are usually handled by techniques like these, which rely on building a type-directed semantic model of the language in some way or the other (though bisimulation techniques are sometimes feasible, too).

I don't see any particular problem with it [type inference for modules].

:) Type inference is already undecidable for plain System F. Modules are more powerful, plus feature a rather involved notion of quasi-dependent subtyping. You don't need any extra complication.

There is a big gap between "type inference is undecidable in general" and "most type inference is pretty much out the window".

My intuition is that it is feasible to develop a library of compositional ad-hoc strategies that can decide most correct programs a human is likely to implement and throw at it. And even where it fails, it might infer the majority of the subprograms. Similarly, strategies can help isolate and describe errors or likely problems, based on a long history.

Under which conditions is decidability essential?

[addendum]

You mention a "type directed semantic model" by which I suppose you refer to type families or similar, and I suppose decidability might be essential for that. But these days I disfavor that sort of implicit program logic (typeful dispatch); I'd rather explicitly model it, e.g. using a reader monad for dependency injection of a set of typeclasses. I'd like to see how far I can get leveraging staged programming with structural types to a similar effect, but using idioms more familiar to dynamically typed programs.

I will try to read your paper next week to see the examples you mention. My list of tabs to clear at the moment is monstrous.

There is a big gap between "type inference is undecidable in general" and "most type inference is pretty much out the window".

Yes, but the crucial point in this case is: type inference cannot deal well with quantified types. On the other hand, quantifiers are the essence of module typing (otherwise you just have plain records and functions). So you won't get far.

You mention a "type directed semantic model" by which I suppose you refer to type families or similar

No, I mean a semantic model of the language that is constructed by induction on types, which is the standard approach to constructing models for typed languages.

First class polymorphism is one answer to that:

http://web.cecs.pdx.edu/~mpj/pubs/fcp.html

Using intersection typings is another (System-I or System-E).

First-class modules imply first-class polymorphism, that is the problem I'm talking about. I'm very well aware of most of the papers on the subject of inference for forms of first-class polymorphism ;) (look at various ICFP papers from the mid-2000's for approaches more flexible than the one you cite there). I assure you that all these methods are far from powerful enough to handle modules. Intersection types don't help either, and come with their own serious set of problems anyway.

I don't want to discourage you from banging your head against the wall, but you have been warned. ;) You're up against 20 years of research.

Every programming language is a set of compromises, for some people and applications a particular set of compromises makes more sense than another. The key is the goals, and my aim is not to take ML style modules with all the features you listed and make them first class entities. My mistake was probably to suggest that records with associated types and named-instances could have all the features of extended ML modules. I am aiming for something much simpler - but other language features should provide the same compile and runtime functionality. Then it all comes down to how well those abstractions fit the problem domain.

I am interested in what you think the problem with intersection types are, because from a type-inference point of view they seem pretty elegant. I don't think the size of the types, or the resources for compilation are a problem with modern equipment, and I find compositional typing to be compelling. Expansion variables provide equivalent functionality to universal and existential quantification, and this paper , http://www.doc.ic.ac.uk/~svb/ITRS02/ENTCS/entcs75104.pdf describes the implementation of a Polar type system that included both intersection-types with expansion variables and universal and existential quantification. Their experience was that when using expansion variables the quantifiers became redundant, and they removed them from the system.

I wonder if quantifiers being 'essential' is due to some other assumed context (separate compilation, implicit ADTs via nominative declarations, imprecise types, etc.).

To me, a module cannot be considered "first class" unless it really is just a plain old value - e.g. functions, row-polymorphic or structural records. If we want ADTs, those must also be first-class, e.g. via sealer/unsealer patterns. I'm not assuming separate compilation (not coupled to modules, anyway). To serve the similar roles as ML modules, we must be able to infer runtime types based on values computed on a compile-time stage, which suggests dependent types or a simplified variation thereof.

a semantic model of the language that is constructed by induction on types, which is the standard approach

It seems to me the dual would be equally reasonable. The idea for pluggable types is that semantics should not depend on type, beyond how primitive functions analyze a shallow structure. But we can presumably infer recursive types based on a semantic model that analyzes values (i.e. recognizing folds and loops). To assert a recursive type would simply be to apply an identity fold.

To me, a module cannot be considered "first class" unless it really is just a plain old value - e.g. functions, row-polymorphic or structural records. If we want ADTs, those must also be first-class

Exactly -- which is what causes the problems with type inference, because it means polymorphism has to be first-class, see above.

It seems to me the dual would be equally reasonable.

No, it won't. To reason about properties established by (or with support from) the type system you usually need a typed model. This is not because the operational semantics is type-dependent itself, but because the semantic guarantees you care about are (e.g., invariants protected by type abstraction).

If we want ADTs, those must also be first-class

which is what causes the problems with type inference, because it means polymorphism has to be first-class

As I understand it, the essential properties of an ADT are that we can:

• control construction of ADT values, i.e. with smart constructors
• control operations on the ADT value, i.e. a constrained set of functions for manipulating it
• temporarily separate the ADT value from some (or all) of the constructors and functions that operate upon it, e.g. pass a list containing values from the ADT to a subprogram that is constrained to operate on the list structure

If we achieve these properties - even if by some non-conventional means - I think it reasonable to say we have ADTs. Do you? AFAICT, you are assuming that ADT properties are enforced by inference of parametric polymorphism, i.e. that the type system was used to achieve this particular semantic guarantee.

Let's consider another approach.

ADT values can be modeled as sealed values. First-class ADT-module objects can then be modeled using records of functions that encapsulate copies of the sealer/unsealer pairs, unsealing values on input and sealing them again on output. These ADT-module objects may themselves be constructed in a first-class manner leveraging stable uniqueness, which can be enforced using substructural types. Thus, the only input is a uniqueness source, and the sealer/unsealer pair need never be exposed to the client who instantiates the module.

In this case, the semantic guarantee of ADTs is achieved constructively, structurally, leveraging simple and universal rules of an object capability model. The type system is irrelevant to this particular guarantee. Gimme ADTs, hold the Ts.

Where the type system gets involved is determining safety and progress properties. For example, it would be very nice to ensure statically that we never pass a value sealed by one instance of a module as an argument to a function from a different instance. If we can infer precise types - such as "this value was sealed by the XYZZY sealer" - then we can make this safety guarantee in an ad-hoc manner (typing the specific use-case). If we can generalize and quantify, we might ensure safety of subprograms in a far more polymorphic manner.

The critical point here is that the inference of quantified types for safety purposes becomes a separate concern from the semantic guarantees we're seeking. The type system is not burdened to establish the properties of ADTs.

To reason about properties established with support from the type system you usually need a typed model.

Many interesting and useful properties can be established using constructive and structural mechanisms orthogonal to the type system. And I expect most of the exceptions have worthy substitutes.

If constructive and structural reasoning are favored exclusively, and types are not used operationally (for dispatch, etc.), then type systems and type inference become pluggable strategies for compositional reasoning about progress and safety. In such a context, it is feasible to incrementally improve and update the type system (to decide more programs, more efficiently and precisely) independently of language updates and the programs.

Sure, you are free to design a language with value sealing. But that won't help you reasoning about modules, which use type-based abstraction (which, btw, happens to be more expressive than value sealing). That was the context of the discussion.

Many interesting and useful properties can be established using constructive and structural mechanisms orthogonal to the type system. And I expect most of the exceptions have worthy substitutes.

Again, this is side-stepping the discussion at hand. Sure, you can try to find typeless substitutes for certain type system features. But types are extremely powerful, and can establish guarantees that you cannot establish by dynamic means. In any case, I have zero interest in turning this into another fruitless typed-vs-untyped debate. ;)

reasoning about modules, which use type-based abstraction [..] That was the context of the discussion.

Are you defining modules as using type-based abstraction? If so, I object.

Modularity conventionally connotes independent development, maintenance, and reuse of subprograms. In a given language, modules should serve modularity, and they might serve a few additional roles and purposes. I don't see abstraction (much less 'type-based') as essential to modularity. Of course, it is useful that we can modularize our abstractions and abstract our modules. But in a perfect language (in my opinion) these roles would be orthogonal.

[type-based abstraction], btw, happens to be more expressive than value sealing

True. Value sealing serves one useful role. Other structural and constructive techniques serve other roles.

I'm rather fond of the "one responsibility rule" in language design. Types in some languages serve a lot of roles, sometimes redundantly: namespaces, implementation hiding, physical representation, abstraction, safety, dispatch, separate compilation, etc.. Classes in C++/Java/etc. are especially egregious.

I can model functions, monads, arrows, frameworks, parser combinators, DSLs, algebraic effects, rows, documents and diagrams, etc. - many kinds of useful abstractions - without reference to the type system.

types are extremely powerful, and can establish guarantees that you cannot establish by dynamic means

Indeed. For example, one cannot guarantee safety or progress or termination by dynamic means. And in a language with partial functions, we could lift 'safety' and 'progress' to proofs on other interesting properties. Types do have a role, but I'm not convinced that 'abstraction' should be one of them.

I think, ideally, that types should be responsible only for those guarantees that cannot be expressed and enforced by dynamic idioms.

Similarly, types are preferable to ad-hoc white box analysis, contracts, and lint-like mechanisms. Those are also extremely powerful, and can establish guarantees that you cannot readily establish by typeful means. But that doesn't mean we should favor them.

Are you defining modules as using type-based abstraction?

ML-style modules, the topic of the subthread, do (as do others). It is an essential part of their expressiveness. Without harvesting the duality between existential and universal quantification and making it seamless you wouldn't get most of the benefits I list above.

I'm rather fond of the "one responsibility rule" in language design. Types in some languages serve a lot of roles

That's a rule I also like (and I share your dislike of classes for this reason). But the granularity of your argument is arbitrary. Yes, "types" serve a lot of roles. But so do "values"! Particular forms of types still serve particular roles. E.g., existential quantification expresses type abstraction. The Curry-Howard isomorphism provides the deeper justification for the various forms of types and their corresponding roles.

In this light, demanding type abstraction be expressed through value sealing/unsealing (instead of existential quantification) is like demanding polymorphic typing be expressed through injections/projections into/from a universal type (instead of universal quantification).

Without harvesting the duality between existential and universal quantification and making it seamless you wouldn't get most of the benefits I list above.

Sure. But my point is that we don't need type-based abstractions to "harvest" this duality.

The Curry-Howard isomorphism provides the deeper justification for the various forms of types and their corresponding roles.

The Curry-Howard isomorphism applies just as well for interpreting computations as proofs. The distinction of 'value' vs. 'type' is not essential.

"types" serve a lot of roles. But so do "values"! Particular forms of types still serve particular roles.

True. Unfortunately, there is a lot of redundancy between types and values (type-level lambdas, records, numbers, objects). Also, as I'm understanding them in context, types are second class - e.g. using type-based techniques, you cannot create a new ADT at runtime based on interaction between server and client. Thus, there are at least two good reasons to favor pushing responsibilities from types to values.

demanding type abstraction be expressed through value sealing/unsealing (instead of existential quantification) is like demanding polymorphic typing be expressed through injections/projections into/from a universal type (instead of universal quantification)

I don't follow the analogy.

I believe that universal quantification corresponds to a subprogram that can operate on any value. What functions do this? Well, taking my bytecode as a concrete example: literal introductions do, e.g. `#42 :: e→N(42)*e`. Identity is universal. Data shuffling is almost universal, e.g. `l :: (a*(b*c))→((a*b)*c)`. And of course function application e.g. of the form: `$ :: (a→b)*(a*e)→(b*e)`.

AFAICT, there is no "universal type" involved, nor do I see any injection/projection happening. There is a value of unknown type, and thus we are very limited on how we can observe/manipulate it.

[addendum]

Sealed values can also enforce universal quantification. We can inject/project to and from a sealed value, and thus control what a subprogram observes.

Universal quantification and existential types don't technically depend on information hiding. They depend only on information ignoring. We can separate the responsibilities of deciding safety of generic usage patterns vs. ensuring security of the data.

But my point is that we don't need type-based abstractions to "harvest" this duality.

I'm not sure what this means.

The Curry-Howard isomorphism applies just as well for interpreting computations as proofs. The distinction of 'value' vs. 'type' is not essential.

Proofs are not relevant by themselves, it's the property they prove that you care about. In any case, the proof for an ADT (in terms of an existential type) is the corresponding existential package. So existential ADTs still are an expression-level construct, if you prefer to look at it from that angle.

AFAICT, there is no "universal type" involved, nor do I see any injection/projection happening. There is a value of unknown type, and thus we are very limited on how we can observe/manipulate it.

That's because you have essentially assumed your own conclusion: that it's best for "polymorphism" to be represented by (implicit) universal quantification. But that's ultimately a design choice. The same holds for type abstraction and existential quantification.

Also, as I'm understanding them in context, types are second class - e.g. using type-based techniques, you cannot create a new ADT at runtime based on interaction between server and client.

Existential types are (or can be) first-class, and hence allow you to treat types in a (sort of) first-class manner.

Universal quantification and existential types don't technically depend on information hiding. They depend only on information ignoring. We can separate the responsibilities of deciding safety of generic usage patterns vs. ensuring security of the data.

This is essentially the question whether polymorphism should be parametric. Parametricity is highly valuable, and you should have very good reasons to break it. But if you cannot afford it for some reason then, yes, you need additional means for enforcing information hiding.

However, that does not imply term-level means! It is most adequately implemented by a type-level mechanism, even in the absence of parametricity -- namely runtime type generativity (see e.g. this paper). In particular, this allows for maximal expressiveness and incurs minimal runtime cost, as opposed to value sealing.

you have essentially assumed your own conclusion: that it's best for "polymorphism" to be represented by (implicit) universal quantification. But that's ultimately a design choice.

My argument hasn't been that "it's best", only that "it's sufficient" towards the goal of first-class modules. Or rather, it's sufficient after we account for a few other language features, such as value sealing, substructural types, capability security, and partial evaluation.

Parametricity is highly valuable, and you should have very good reasons to break it.

Parametric polymorphism can be enforced by value sealing, and expressed by simply not observing a value. The means of enforcement is perhaps less convenient than leveraging a type system, but I wouldn't call it 'broken'.

Also, I haven't really missed the more convenient enforcement. It seems a few of parametricity's use cases are well enough addressed by substructural types or capability security, or simply having a unit value that may not be observed. I can't think of much reason to enforce parametric polymorphism other than to prove that I can do so. The discipline of expressing generic programs, OTOH, is valuable for reuse reasons.

[runtime type generation] allows for maximal expressiveness and incurs minimal runtime cost, as opposed to value sealing

Value sealing also has minimal runtime cost, unless implemented most naively. I expect the cost is commensurate with runtime type generation.

My argument hasn't been that "it's best", only that "it's sufficient" towards the goal of first-class modules.

Just like it is "sufficient" to use existential quantification for type abstraction. I still think you are making an arbitrary distinction.

Parametricity is highly valuable, and you should have very good reasons to break it.

Parametric polymorphism can be enforced by value sealing, and expressed by simply not observing a value. The means of enforcement is perhaps less convenient than leveraging a type system, but I wouldn't call it 'broken'.

I meant breaking the parametricity property of the type system (and thereby precluding, for example, a parametric model for the language, and any reasoning based on that).

It seems a few of parametricity's use cases are well enough addressed by substructural types or capability security, or simply having a unit value that may not be observed.

What use cases are these? Do you have a reference?

Value sealing also has minimal runtime cost, unless implemented most naively. I expect the cost is commensurate with runtime type generation.

No, because value sealing generally requires deep copying (and wrapping functions in the higher-order case), whereas type-based sealing usually does not. That also implies, btw, that value sealing does not support abstracting the contents of mutable state or other impure or identity-aware data structures.

Just like it is "sufficient" to use existential quantification for type abstraction.

True. I haven't argued otherwise. But, because you depend on type abstraction, you're also depending on type inference, and thus you're more vulnerable to conditions where types might be difficult to decide.

By relying on an alternative to type abstraction, I have more flexibility to reason about software even in cases where types are not fully decided. I can't say this is better or worse than a typeful approach. But it has different properties, which may be useful in different contexts, such as first-class modules.

I meant breaking the parametricity property of the type system (and thereby precluding, for example, a parametric model for the language, and any reasoning based on that).

Then how is your argument relevant? What value do I lose in the case you preclude?

What use cases are these? Do you have a reference?

Linear control flow, composition of pipeline abstractions, use of a callback method, etc.. I don't have a reference.

value sealing generally requires deep copying

This hasn't been my experience, but perhaps I've created a context where value sealing is cheap: no pervasive mutable state, ability to control aliasing via substructural types.

value sealing does not support abstracting the contents of mutable state or other impure or identity-aware data structures

Sure. Value sealing isn't a big hammer. It is useful to enforce parametricity, which seems to be your big hammer. But, with value sealing, I need orthogonal mechanisms to abstract state and identity. Access to mutable state is abstracted through capabilities. Identity can be enforced through substructural types.

But, because you depend on type abstraction, you're also depending on type inference

I don't understand what you mean. Using the type system for abstraction certainly does not require type inference.

I meant breaking the parametricity property of the type system (and thereby precluding, for example, a parametric model for the language, and any reasoning based on that).

Then how is your argument relevant? What value do I lose in the case you preclude?

What do you mean? As I said, you lose a simple semantic model and a very powerful reasoning principle, as well as useful abstraction properties ("Theorems for free" and so on). I care about that, YMMV.

Using the type system for abstraction certainly does not require type inference.

Apologies. I said 'type inference', but I meant decidable computation of types in general. Ultimately, you're depending on the type system to express or enforce properties that cannot be directly expressed or enforced at the term level. Thus, if you fail to type a program, you lose most of your ability to reason about those properties.

you lose a simple semantic model and a very powerful reasoning principle, as well as useful abstraction properties ("Theorems for free" and so on). I care about that, YMMV.

I have a different simple semantic model, powerful reasoning principles, and useful abstraction properties. I enjoy "theorems for free" and "correctness by construction".

I care about that. But I don't believe expression of parametric models - much less specifically via the type system - is a necessary condition for these features. There are other means to the same ends.

I said 'type inference', but I meant decidable computation of types in general.

That's also independent.

Ultimately, you're depending on the type system to express or enforce properties that cannot be directly expressed or enforced at the term level.

Yes, that's a feature. ;)

I have a different simple semantic model, powerful reasoning principles, and useful abstraction properties. I enjoy "theorems for free" and "correctness by construction".

That sounds mysterious, as I am not aware of any other semantic technique (except perhaps brute-force bisimulations) that can give you something similar. Do you have a reference?

You aren't even aware of the strong reasoning properties and theorems enforceable by capability security or linear values? I've mentioned them. Or do you believe these techniques are somehow not semantic in nature?

Are you sure you're talking about formal reasoning, and not just informal considerations?

Because as far as I can tell, these features allow you to strengthen your models in certain ways, but they don't free you from having to construct these models if you want to do the kind of reasoning I'm talking about (e.g., interesting program equivalences and abstraction properties). When you design a language such that you cannot easily build a useful model in the first place, then I don't see how adding any clever feature can help -- unless there exist some advanced formal techniques that I've never heard of (in which case I'd dearly like to see a reference).

Are you sure you're talking about formal reasoning, and not just informal considerations?

Yes. Formal reasoning is imminently concerned with the 'form' (shape, structure, pattern or signature) of an argument/proof/protocol/program, and how these forms may be composed, manipulated, validated or reasoned about, and executed. Capabilities, linearity, spatial idempotence, causal commutativity, value sealing, and a variety of other structures are all deeply formal.

They aren't necessarily "denotational", however. The concept of "denotation" implies an additional step of translating from one form form to another - a 'meaning' that is separate from the original 'form'.

these features [..] don't free you from having to construct these models if you want to do the kind of reasoning I'm talking about (e.g., interesting program equivalences and abstraction properties)

With capabilities and value sealing, I can reason about equivalencies in accessibility or authority of a subprogram without knowing its implementation details (i.e. abstraction). With linearity, I can reason about equivalencies (and some useful in-equivalencies) in resource use or protocol completion. With spatial idempotence and causal commutativity, I can reason about equivalencies in program structure and syntax. I can reason about boundaries and trusted paths and visibility and more.

There are a great many interesting program equivalencies and abstraction properties that I can reason about, all of them structural and formal.

When you design a language such that you cannot easily build a useful model in the first place, then I don't see how adding any clever feature can help

I agree. It would be silly to create a language that makes it difficult to build useful models.

unless there exist some advanced formal techniques that I've never heard of (in which case I'd dearly like to see a reference)

Perhaps you should review the formal techniques you've heard of but never deeply explored, rather than dismissing them as implementation details that merely 'strengthen' models that you choose primarily to express and enforce via separate type system.

Please be so friendly to provide at least one reference that would demonstrate how one formally proves, say, representation independence, by exploiting those constructs but without using logical relations or bisimulation techniques.

There is a difference between:

• formally reasoning about P in context of a language/logic L
• formally proving in general that L, through some features F, allows you to formally control/reason about P

My impression is that you're asking for the latter despite the former being both necessary and sufficient for formal reasoning.

Object capabilities and sealed values are essentially primitive forms for representation hiding. They can axiomatically be used to formally reason about representation independence, but their ability to do so cannot be proven from within the same logic. You might as well ask for a formal proof of modus ponens by exploiting the constructs of classical logic. What would you say to such a request, assuming it came from an intelligent person that you respect?

For a different P, there was recent mention of a paper on proving functional purity from method signatures in a capability-secure restricted form of Java called Joe-E. Though, the ambient authority to allocate local state does complicate reasoning about purity for Joe-E and more conventional ocap languages.

To stick to the representation independence example, you usually only do the former, using some sufficiently powerful proof technique. The latter would be some form of completeness result for that technique -- but often enough no known technique is complete, and where it is it doesn't necessarily imply practical feasibility.

As modules declare an interface defined by its types, which represents a contract between client and implementation, that the implementations will conform to the type contract, allowing the clients to rely on the types the functions, any inference of the contract types would defeat the point of having the contract in the first place. So if there were one place in a program where you wanted to specify types for functions, the module definition would be it.

some forms of formal reasoning about programs might become next to impossible

Which forms? Can you provide one or two examples? Or is this just a hypothetical possibility?

I'm very fond of formal reasoning. I'm especially fond of two classes thereof: compositional reasoning (which describes properties of a group as invariant or inductive over a set of composition operators) and equational reasoning (which describes two expressions of a subprogram as equivalent with respect to external observations). My recent language designs enforce a number of properties to simplify formal reasoning: capability security, causal commutativity, spatial idempotence, and substructural types.

My observation is that a great deal of formal reasoning is feasible even for code laden with effects, divergence, and partial functions.

Some approaches to expressing systems - e.g. use of events and messages or local state - do seem problematic for reasoning in context of open systems or concurrency. But we can find other ways to express effects, and the reasoning issues with common effects models seem orthogonal to any type system issue.

The undecidabilty only affects type classes with recursive definitions (undecidable-instances). So I think you can use records and records as modules (with named-instances) without any undecidabilty. The problem is only when using instances implicitly, and then only with recursive instance definitions. There are practical ways to deal with this like finite-depth restriction, or restrictions on recursive instances. Is restricting instances to structural recursion enough to keep things decidable?

Isn't it better to have an undecidable static computation - i.e. when the programmer is around to evaluate and debug - than an undecidable runtime computation?

Probably. But it is required to be able to know (conservatively) which computations are decidable. Without that, you cannot know when it is safe to stop adding annotations.

I think it is more subtle than that. Unification with unrestricted intersection types is undecidable, but when using type inference on lambda calculus, will you generate any non-unifying terms? So although something may be undecidable in theory, you may not ever encounter that case in practice. In many cases a finite-rank restriction is all that is needed. If unification does not converge in 'N' iterations (where N is a compiler argument) seems a satisfactory solution in practice, where the chances of a non-terminating case are low (obviously if it does not terminate on common code idioms then that is no good).

Out of interest does anybody know any lambda terms that cause non-termination of type inference System-I or System-E?

I'm not an expert but my understanding of (non-rank-limited) intersection types is that they are powerful enough to type any normalizing term, and that in fact providing an intersection typing amounts to performing normalization.

In their 2004 paper on type inference for System E, Type inference with expansion variables and intersection types in System E and an exact correspondence with beta-reduction, Sébastien Carlier and Joe B. Wells carefully design an inference algorithm for System E to make the correspondence between inference (in fact unification) and beta-reduction precise, with some steps of constraint solving corresponding precisely to program evaluation.

It is not *obvious* (to me at least) that this implies that the inference algorithm never halts on non-terminating term (some form of non-termination might be recognized by the algorithm, ruling out classic non-terminating lambda-terms as an example), but on closer examination the paper does say so:

Let M be an arbitrarily chosen λ-term. If M has a β-normal form, then the procedure described below will terminate, otherwise it will go forever

It says other things that are not in line with the view of intersection types you present in this thread, but it may be the case that further work on expansion variables strengthened their confidence in the usability of intersection type systems for general programming, as you express.

Because types are often exposed to programmers, a major design goal for many type systems has been making types suitable for human comprehension. Unfortunately, this conflicts with making types suitable for accurate and flexible program analysis. Intersection types are good for accurate analysis. However, inferred intersection types may be extremely detailed and thus are likely to be unsuitable for pre- senting to humans. Alternative type error reporting methods such as type error slicing [15, 16] can avoid presenting these types directly to programmers. Investigation is needed to combine type error slicing with System E.

Module boundary interfaces are generally intended to abstract away from the actual software on either side of the interface, so that implementations can be switched. Also, module boundary interfaces must be compact and easily understandable by humans. For these reasons, ∀ and ∃ quantifiers are appropriate for use in module boundary types.

In the paper "Implementing Compositional Analysis Using Intersection Types With Expansion Variables" there is the following quote "In addition, for each natural number k, typability in the rank-k restriction of System-I is decidable, so a complete and terminating analysis algorithm exists for the rank-k restriction.". They go on to provide an algorithm for calculating the rank from inspecting the types, so that for any program the algorithm is decidable, as a limit for k is found before each unification.

The paper on polar type inference for system-i uses quantified types for requirements, and intersection types for capacities. Later in the paper they remove the quantified types as the expansion variables are serving a similar purpose. Note this means the expansion variables remain in the types presented to the programmer, so this may be confusing at first. I have yet to do enough to determine whether I like it yet.

They go on to provide an algorithm for calculating the rank from inspecting the types, so that for any program the algorithm is decidable, as a limit for k is found before each unification.

I'm not sure what you mean here. If you meant that for any term, you can guess "in advance" the maximum rank you need to use, then I suspect it is wrong; you can read back the maximum rank by inspecting the type of a well-typed program, but (at least in System E) only normalizing programs have a type so this won't work for input programs that may or may not be typeable.

I'm not sure which part of the paper you're talking about; section 3.10 (Keeping Track of the Global Rank) explains how to compute the maximal rank happening in a inference constraint that is currently being solved, so that the rank-k-limited variant can stop (reporting failure) as soon as the global rank exceeds k. This means that any k-restriction of the type system is workable in practice and can be explicit about where the k-limitation is broken -- which may be what you describe in your answer.

This is correct, my description above is wrong in suggesting it could be worked out in advance.

Well, one of the fundamental results of the module literature is that you can have either first-class modules (along the lines you sketch) or a decidable type system, but not both.

What sorts of modular semantics can't be decidably checked when the modules are first-class?

This sounds like a it would make a good survey paper for language designers and enthusiasts, if one doesn't already exist.

Subtyping of module types becomes undecidable when abstract type components can be instantiated with module types themselves -- see Mark Lillibridge's thesis (1997) for details. FWIW, you can construct an analogous example to demonstrate that module type checking in OCaml is undecidable as well, due to abstract signature specifications. In both cases, you probably won't run into these examples in practice. But as I alluded to above, it seems to preclude an obvious semantic model for the language, which I personally find bothersome.

(Edit: The first chapter of Derek Dreyer's thesis (2005) contains a bit of a survey on ML module theories, it mentions undecidability of Harper/Lillibridge's system in Section 1.2.3. We also have a brief discussion of first-classness in the draft journal version of our F-ing modules paper (2013), see Section 6.1.)

I haven't done the job of looking at this termination problem in the eyes, so I'm not quite sure of what I will say. But I suspect it is related, in dependently typed languages, to the inconsistency that arises when you mix impredicative polymorphism (as in system F and ML modules) and "strong sums", that is dependent sums with a first projection behaving as you could expect -- instead of only an existential-like elimination principle.

I'm telling this because it may help people that think of module systems as glorified dependent records to get an idea of what kind of problems we run into, even in ML languages.

I was thinking of something like this paper: http://research.microsoft.com/pubs/67016/first_class_modules.pdf

It depends on what you are still willing to call "modules". ;) That paper provided a fairly simplistic system, which of course is an advantage. But it also did not provide most of the power and expressiveness of real modules. In particular, it described an approach that requires manually shuffling around quantifiers (especially existentials), which is known to not scale very well to less-than-trivial modular architectures.

I am prepared to call a record with associated types a module. It should have all the power of Haskell type classes with dependent types, so that's good enough for me. What would I be missing out on?

The essence of modules is implicit existential and universal quantification over those "associated" types. In the approach you have in mind, most of these quantifiers have to be introduced and eliminated explicitly, and repeatedly so -- you are basically programming directly in something akin to System F. The most important role of modules, as far as I'm concerned, is to abstract away from this fairly low level approach. You are also missing out on most of the other features I listed earlier.

In essence, modules are a higher-level programming language, whereas System F is the analogy of an "assembly language" with respect to handling complex types. So in a way, you certainly can express "everything", but the extra manual bookkeeping is verbose and quickly becomes impractical.

I can see the need for existential quantification for hiding types inside the module, but that could be provided by some syntactic sugar like "private data", so inside the instance definition the unquantified type is available. The externally visible associated types behave exactly like type classes with a one-way functional-dependency which means for most cases selecting the instance is enough to resolve the type. It seems to me the bookkeeping could be automated for records in a similar way to modules. Type inference would work as in Haskell with type-classes and functional dependancies.

Perhaps functions could provide local datatype definitions by automatic existential quantification? Allowing for a hastily thought up syntax:

(inj, proj) = {Test a = Test a} (inject x = Test x, project (Test x) = x)

print ((proj . inj) "Test")

inside f the datatype behaves as data Test a = Test a, outside as if it were not in scope.

...though I know too little about the nature of that inconsistency to tell.

Subtyping may not be necessary. Polymorphic functions, and overloaded dispatch constrained by type-classes (modules / records) provide the needed structure, provided you only need static (compile time) polymorphism.

Well, the hard part of subtyping here is not width subtyping on records/modules, but the crucial instantiation relation on "associated types". If you remove that then I'm not sure what is left of "modules". And type classes don't provide first-class instances either, so I don't see how they would solve that specific problem.

Associated types are restricted form of functional dependencies used in Haskell type classes. Type classes are implemented with implicit dictionary passing (so the semantics are the same). A dictionary is just a record of functions, so the equivalence is there in the implementation. Replace the implicit dictionary with an explicit one and you have records. Records are already first class. So the only difference between a record and a type-class is the overload resolution by which an instance is selected when implicit (In Haskell overload resolution for instances is done using unification, and hence the type system is actually a logic programming language, I don't see any need to change that, but how instances come into and out of scope might be different).

Thanks for your detailed response above, I have some interesting reading to do. The blurb in your most recent paper gave me an idea of what's going on.

Re: associated types and type classes not providing first-class instances. What about Objects to Unify Type Classes and GADTs, which does lift type classes to first-class types. Once you add associated types, this would seem to provide what you're looking for in a module system. What would be missing? The paper has a short section that discusses extensions to modules, but it's very limited and there's no follow-up as yet.

The object system in "Objects to Unify Type Classes and GADTs" looks like the kind of thing I am thinking of, with the addition of associated types.

This paper ML Modules and Haskell Type Classes: A Constructive Comparison claims a translation is possible between ML modules and Haskell type classes by adding "abstract associated type synonyms".

So Stefan Wehr and Manuel M.T. Chakravarty's abstract associated type synonyms added to Bruno C. d. S. Oliveira and Martin Sulzmann's objects would seem to give me what I wanted when I referred to "records with associated types and named instances".

What do you think of this approach, Can you see any obvious problems?

I'm aware of this paper, but like a lot of discussions along these lines, it only considers a couple of very trivial examples. There are at least two fundamental problems with the sketched translation: (1) it only applies to a very restricted subset of the module language, and there are many aspects you cannot encode this way, e.g., nested modules, higher-order functors, sharing constraints, more general uses of sealing, local modules, etc.; (2) it replaces the structural typing and subtyping of modules with the nominal typing of classes and datatypes, which destroys almost all of the modular expressiveness even for the sublanguage they consider.

What all these attempts have in common is, in summary, that they sacrifice most of the compositionality of ML modules, which is their primary source of expressive power.

(PS: I also doubt that you can easily combine the two papers you mention into one system without running into serious problems, especially wrt abstract types.)

What's your perspective on the relative success of Haskell in so many domains, despite lacking the features of the ML module system that you imply are so important? Will the lack of modules ultimately limit Haskell in some way?

I understand some of the localized impacts due to poor module systems, but there seem to be so many sufficient workarounds that it's not clear whether these missing module features are ultimately limiting, and thus the drive towards ML modules is just theoretical aesthetics.

C++ has a terrible modularity story and is arguably a wide success. It's hard to deduce anything about language design based on "relative success".

You may not have heard about Backpack, which is Scott Kilpatrick's PhD work about backporting the main ideas from Andreas's (and Derek Dreyer's) MixML into a kind of module system for Haskell. It is evidently of high interest to Haskell designers, which are well aware of the current deficits of Haskell in that respect, and of the can of worms they avoided opening for so long.

I'm in the process of realizing that Backpack doesn't seem to have been feature on LtU yet. Running to the submission page.

Backpack sounds really exciting, even though I'm used to wimpy module systems, as in what Haskell offers.

I'm surprised that parametric modules haven't had a bigger impact on functional programming languages yet (can't think of any other than SML, OCaml and Ur/Web off the top of my head, maybe Scala counts as having the feature?).

Thanks for the Backpack reference. I think I had come across it on reddit, but I didn't have time to look at it in detail.

The more I think about this, the more I am coming round to the ML approach. If its not safe for modules to be first class (and I now think that is the right thing as I would want them to be types, not values), am I right in assuming implementations of modules are simple first class values? Apologies if I am being a bit slow getting this, as I come more from a Haskell and C++ background and haven't looked at ML much. We can apply the mapping from modules to type-classes the other way around, and we should be able to map all of Haskell type-classes into ML modules? Modules can also function as records? If so then this is what I am looking for, a single concept that encompasses records, type-classes and modules.

Edit: I have realised I am having a problem with terminology. When I say above "modules should be types" I am referring to what ML calls "signatures".

I should point out that I am using something like the ML module types for functions, as I have completely compositional HM type inference with principal typings, where functions have type judgements instead of types. This is completely decidable (unlike unrestricted intersection types) but also supports separate compilation because type inference composes.

I understand the issues with type-equivalence vs value-equivalence, and pure vs impure functors, however is it avoidable? Equality is not defined for functions and they are first class. Functions would have the same problem if we allowed them to be 'packed'. The issue appears not to be with functors being first class, but the existence of pack/unpack.

If we require impure code to be in a monad, then that also resolves the applicative, generative problem. Impure functions would be in the IO monad and can only return results generatively.

These two issues appear specific to the design on ML, and not something that affects PL design in general. For my purposes I am happy to have opaque function definitions (where functors == functions, and modules == records), and I intend to have more fine grained effect control than just an IO monad, I am looking at something like row-types to manage effects, where different resource types are tracked separately, even individual memory regions tracked separately.

Edit: I realise my understanding of pack/unpack was wrong here, I thought is was (de)serialising the module, but it appears be more like an 'unrun' operation.

I'm not sure I fully understand the question. What do you mean by "functions being packed"? Since you mention pure vs impure functors, may I assume that you are referring to the F-ing modules semantics?

It is true that impure/generative functors become obsolete if your language is pure, i.e., impurity is at least monadically encapsulated, and if you didn't support packaging up modules as first-class values.

But you still need to take value equivalence into account for type equivalence if you want safe abstraction. You cannot get rid of having some notion of equality on functors either, since you need to be able to denote and compare types like Set(Int).t, for example. Otherwise, you would effectively have only generative functors. Maybe that's what you want?

Yes, I was looking at the F-ing module semantics. It seems to me all the issues with generative and applicative are solved by a pure language with monads. The monad itself is a value and can be passed around and assigned as a value, but to execute the program it contains it has to be explicitly 'run' which does the generative bit.

That depends on what exactly you mean by "all issues". ;)

Edit: Pack/unpack is not related to (dynamic) effects, and is no "unrun" operation. It merely wraps up a (second-class) module as a first-class value. This explicit operation is necessary (even if the module is pure) to keep the core language type system cleanly separated from the module type system, and avoid all the issues I alluded to earlier.

There is still the issue with associated types, where we require module instances to have different types if they are to be passed as values. Adding the associated types as phantom types to the module instance type would be a solution to that - which I think you mentioned in the F-ing modules.

So with the type system I am using, the pure applicative modules with no associated types are just plain records. Associated type synonyms should be fairly easy to add with phantom types and I may as well add them to records. Impure generative modules will be achieved by encapsulating the record and state in a monad.

An interesting thought is that associated types when encoded into phantom types are a form of output type parameter and might be more easily expressed as type level functions. The signature establishes the kind of the type level function and the instances define a partial function on types. This functionality gets duplicated in type-families.

So I think with simple Haskell style modules to provide encapsulation, type-classes (with named instances) for overload resolution and type-families for type level functions you can get the same expressive power as modules. Noting that the role of the environment in module type judgements is taken by type constraints from type-classes.

Okay, so pack/unpack would be unnecessary with the type system I am using, as every term has a typing, and is not necessary in Haskell because it has type constraints.

Ordering is a great example, because it's something you can explain to everybody. There are lots of other examples, including a whole bunch in the area of I/O. Named instances are a precondition to any solution, because choice requires designation. But named instances are not a solution in and of themselves.

Note that once you have multiple instances you lose a bunch of subsumption properties. Consider that any implementation of "sort" over a vector is going to rely on Ord over the index (of type int or Nat), and also Ord over the element type 'a. When the element type 'a turns out to be int or Nat, it does not follow that the two uses of Ord int and Ord 'a = int can correctly be merged/simplified.

I think what you are saying is you may have to pass two dictionaries, because you cannot tell from the type system that they are the same, and if you are allowing runtime polymorphism they have to be separate as they could differ at runtime. In the static case is should be fairly easy to compare the actual dictionaries for equality, or even the actual methods in the dictionary. A unique-id could be added to each definition when bound to the symbol by the compiler, so sort would know the 'less_than' function is the same definition no matter which dictionary supplied it, as even if the types are the same they could actually be different functions.

...otherwise I agree with everything you said. :)

One thing to note perhaps is that polymorphic recursion in OCaml is a relatively recent addition, other than in Haskell.

I can think of safe uses for higher ranked types that do not make monomorphising impossible like:

f (\id :: forall . a -> a) = (id 'a', id True)

So it seems to me that some restriction on higher ranked types world make this workable. The worst case is to just have a depth limit on recursion in the monomorphisation. Can it be done better than this? Can we know in type inference/checking whether the set of monomorphised functions are finite?

Also isn't there another view of type-classes as constraints on types like in HM(X)?

It's somewhat simple. Deriving a type from a value doesn't equal deriving a value from a type.

You got the C++ RTTI mechanism wrong.

(Maybe a bit harsh. I get what you're doing. What is global information becomes local information, becomes the argument of a function. But you flattened out the conceptual difference between type classes and interfaces. Peeling off a value from a type versus peeling off a type from a value.)

Lets see if I understand this. When you require an instance of a type-class (without named instances, which is the current standard) the instance selected is completely determined by the type parameters, in the simple case of no functional dependancies (or associated types) the type class completely determines the type of the function, and the instance selected is irrelevant to the type-system. In the more complex case associated types are determined as if by a partial function on types, so there is no need to convert a value to a type. The type signatures of the functions in a type-class are completely determined by the type signatures available in the class definition (which is part of a global polymorphic environment) and the type parameters which occur as a constraint on the type of the function using the type-class, which must be resolved at compile time.

I think I now understand what is going on in the case of polymorphic-recursion. If there are no associated types (or no functional dependancies) then the type of the instance is completely determined by the type of the type class, we know (==) :: a -> a -> Bool and nothing depends on the instance selected (as far as the type system is concerned). It will not work with associated types (or functional dependancies) and testing seems to confirm this.

With named instances can be selected by a value (where all the values have the same type) in the absence of functional dependancies and associated types, but if we require these the instance name must passed as a type-level label (IE a constructor for a singleton type). Both of these allow instances to be first class values that can be passed to functions, the only difference is the type of the selector.

All of this should be the same for modules, leaving purity of the language aside as that is another difference between Haskell and ML that is orthogonal to type-classes vs modules. For a pure language and applicative modules, in the absence of associated types the module type is completely determined by the signature and its parameters like a type-class, and instance selection by values of the same time would work. Adding associated types we require modules instances to have distinct types (phantom types) or singleton type instance selectors.

So irrespective of whether module or type class, the presence of associated types requires type-indexed-instances. In the absence of associated types value-indexed-instances are okay. So we can make type-classes first class providing we observe these rules, which would effectively make pure applicative modules and type-classes the same thing, providing we allow for modules to be made type-safe by following the same rules regarding the type of the first class value with associated types.

A final thought is that this would suggest that associated types used with polymorphic recursion are unsafe, but of course type-indexed instance selection would prevent this from passing type checking, and indeed Haskell will not accept this case.

Consider this:

data X a = Leaf a | Nested (X [a])

An element of X is either an a, or list of a, or list of lists of a, etc. We could define a function 'xsize' that returns the total number of leaves.

xsize :: X a -> Int 
xsize = xmap (const 1) (\f xs -> sum (map f xs))

xmap :: (a -> r) -> (forall b. (b -> r) -> [b] -> r) -> X a -> r
xmap f g (Leaf x) = f x
xmap f g (Nested xs) = xmap (g f) g xs

How would you monomorphize that? Do you consider this to be problematic?

This would not be problematic. There are no types that depend on values. There are two separate things, the problem above is a type safety problem that means it is possible to write code that crashes at runtime if you combine value dependant types (from polymorphic recursion), type classes or modules and associated types or functional dependencies.

The monomorphisation issue is separate, and I would use runtime polymorphism for this. What I want is a clearly defined subset of the language for which monomorphisation is possible, and understand if type-inference can be used to tell the difference.

OK, I didn't understand that there were two separate issues, but I'm still confused. I think it's probably more naming issues, so let me just go through and describe the situation in what I think is standard terminology.

Types don't ever depend on values in Haskell, by construction. Types can be inferred, based on value-level expressions, but they still don't depend on actual values.

Instances are selected based on types & type constraints and the mechanism by which this happens doesn't depend on actual values, either. You can, however, arrange for instances to be passed around first class, i.e. in such a way that which instance you have in a particular variable does depend on run-time values. But instances are not types. We're not passing types around first class -- only instances.

Passing around instances first class doesn't require polymorphic recursion. For one, you can enable existential types as an extension and write something like this:

data Foo a = forall a. Class a => Foo a

That pretty much just says "Foo a carries an instance of Class around with it as a value." Using a continuation passing style, you can encode something like that with higher rank functions instead. But either of those approaches is an extension over Haskell 98, as I recall.

The only thing that I can see that polymorphic recursion does is block a certain type of optimization/implementation technique whereby you would inline/monomorphize everything in sight.

Your analysis leaves out the effect of functional dependancies (or assiciated types). Sticking to how this problem manifests in Haskell (and ghc does detect and prevent this as far as I can tell). If you have a type class with a fundep, then the type of the dependant type varys with the selected instance. Although the type system knows which class will be used (Eq a in the earlier example of polymorphic recursion) it does not know which instance until runtime. Normally this does not matter as in Eq a, all instances of Eq share the same polymorphic type. However if a type class with a fundep is used instead then the type of the dependant parameter can be changed by which instance is selected, and any type level computation could be changed by that result, so you would end up with static properties being changed by a runtime value. Obviously you can't allow this, and Haskell reports an 'ambiguous type variable' and fails to compile.

and any type level computation could be changed by that result, so you would end up with static properties being changed by a runtime value.

"Static properties changed by a run-time value" is an oxymoron. The situation with associated types doesn't seem to me to be much different than the situation with existentials -- you're passing around handlers that know how to deal with an unknown concrete type. I don't remember what causes ghc to complain 'ambiguous type variable', but it's not illegal instance dependence on a run-time value. At least, that's not the way ghc will look at it. Do you have a small code snippet that produces the error?

Here is an example, that also shows the existential case:

#!/usr/bin/env runhaskell -XRankNTypes -XMultiParamTypeClasses -XFunctionalDependencies -XFlexibleInstances -XFlexibleInstances -XUndecidableInstances -XExistentialQuantification

class Count a where
    count :: a -> Int
instance Count () where
    count () = 0
instance Count a => Count [a] where
    count [x] = 1 + count x

class (Count x, Count y, Count z) => Add x y z | x y -> z where
    add :: x -> y -> z
instance Count x => Add () x x where
    add () x = x
instance Add x y z => Add [x] y [z] where
    add [x] y = [add x y]

data Box1 = forall a . Count a => Box1 a
data Box2 = forall a b . (Add a a b, Count b) => Box2 a

f0 :: Count a => a -> Int
f0 x = count x

f1 :: (Add a a b, Count b) => a -> Int
f1 x = count $ add x x

f2 :: Count a => Int -> a -> Int
f2 0 x = count x
f2 n x = f2 (n-1) [x]
{-
f3 :: (Add a a b, Count b) => Int -> a -> Int
f3 0 x = count $ add x x
f3 n x = f3 (n-1) [x]
-}
main = do
    case Box1 [()] of {Box1 n -> print $ count n}
    case Box2 [[()]] of {Box2 n -> print $ count (add n n)}
    print $ f0 [[[()]]]
    print $ f1 [[[[()]]]]
    x <- getLine
    print $ f2 (read x) ()
--  print $ f3 (read x) () 
    case (if (read x < 1) then Box1 [()] else Box1 [[()]]) of {Box1 n -> print $ count n}
    case (if (read x < 1) then Box2 [()] else Box2 [[()]]) of {Box2 n -> print $ count $ add n n}

This shows existentials are okay, if you try uncommenting 'f3' you get an error like:

    Could not deduce (Count z) arising from a use of `f3'
    from the context (Add a a b, Count b)
      bound by the type signature for
                 f3 :: (Add a a b, Count b) => Int -> a -> Int
      at test.hs:30:7-45
    The type variable `z' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there are several potential instances:
      instance Count a => Count [a] -- Defined at test.hs:7:10
      instance Count () -- Defined at test.hs:5:10
    In the expression: f3 (n - 1) [x]

Notice that the type constraints for 'f1' and 'Box2' are the same as 'f3', and where we know the type of 'a' at compile time, we can determine the type of the functionally dependant type variable 'b' at compile time, which is okay, but in 'f3' where we cannot know the type of 'a' at compile time, and we cannot check values of a from () to infinity.

The issue is not what is happening with dictionaries when the program is running, but what is happening in the type-system during compilation. Depending on how you view this, this is either the type system rejecting a program that should run okay (if you define the language by its runtime implementation), or the type system rejecting a program it cannot complete the analysis of because it would need to check the infinite set of (), [()], [[()]], [[[()]]]... in the definition of 'f3'. In the last line, the case with Box2, although which path is taken is not known until runtime, both paths can be statically type checked at compile time. So the problem with the polymorphic recursion example is that it requires type checking of an infinite set of paths. Could a smarter type-checker solve the polymorphic recursion by induction?

Thinking of it requiring type checking an infinite set of paths statically probably makes more sense, but when I was referring to a static property depending on a runtime value, this is the other way of thinking about it. You end up requiring staged compilation, so you partition the program, deferring type-checking and compilation of part of the program until after the user has entered the value. This relates to dependently types languages, which require staged compilation, dynamic code generation, or an interpreter.

Depending on how you view this, this is either the type system rejecting a program that should run okay (if you define the language by its runtime implementation), or the type system rejecting a program it cannot complete the analysis of because it would need to check the infinite set of (), [()], [[()]], [[[()]]]...

I view it neither of those ways. Look at this definition:

f3 :: Add a a b => Int -> a -> Int
f3 0 x = count $ add x x
f3 n x = f3 (n-1) [x]

The definition of 'f3' here assumes a particular context in which this function has to work. The compiler is only allowed to know that a and b are types which satisfy (Add a a b). The compiler attempts to work out a derivation of (Add [a] [a] c) and it cannot, because it's not possible. Try adding this additional (overlapping) instance for Add and see if it does what you want:

instance Add x y z => Add x [y] [z] where
    add x [y] = [add x y]

First, adding this instance breaks the existential with the literal, the 'f1' version and, the existential with add.

test.hs:44:10:
    No instance for (Count z) arising from a use of `Box2'
    The type variable `z' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there are several potential instances:
      instance Count a => Count [a] -- Defined at test.hs:7:10
      instance Count () -- Defined at test.hs:5:10
    In the expression: Box2 [[()]]
    In a stmt of a 'do' block:
      case Box2 [[()]] of { Box2 n -> print $ count (add n n) }
    In the expression:
      do { case Box1 [()] of { Box1 n -> print $ count n };
           case Box2 [[...]] of { Box2 n -> print $ count (add n n) };
           print $ f0 [[[...]]];
           print $ f1 [[[...]]];
           .... }

test.hs:46:13:
    No instance for (Count z1) arising from a use of `f1'
    The type variable `z1' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there are several potential instances:
      instance Count a => Count [a] -- Defined at test.hs:7:10
      instance Count () -- Defined at test.hs:5:10
    In the second argument of `($)', namely `f1 [[[[()]]]]'
    In a stmt of a 'do' block: print $ f1 [[[[()]]]]
    In the expression:
      do { case Box1 [()] of { Box1 n -> print $ count n };
           case Box2 [[...]] of { Box2 n -> print $ count (add n n) };
           print $ f0 [[[...]]];
           print $ f1 [[[...]]];
           .... }

test.hs:51:32:
    No instance for (Count z2) arising from a use of `Box2'
    The type variable `z2' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there are several potential instances:
      instance Count a => Count [a] -- Defined at test.hs:7:10
      instance Count () -- Defined at test.hs:5:10
    In the expression: Box2 [()]
    In the expression:
      (if (read x  print $ count $ add n n }

So that is no help. Besides Add [a] [a] c matches the instance Add [x] y [z] by unification with x = a, y = [a], [z] = c just fine.

I think I can get it to work out the missing constraint by modifying the type class definition of Add to:

class (Count x, Count y, Count [z]) => Add x y z | x y -> z where
    add :: x -> y -> z

Which requires -XFlexibleContexts and should allow the missing count constraint to be inferred from Add. Adding this everything that was working before still works (provided flexible contexts are enables) but we still get an error for 'f3':

    Overlapping instances for Count [z] arising from a use of `f3'
    Matching givens (or their superclasses):
      (Add a a b)
        bound by the type signature for
                   f3 :: (Add a a b, Count b) => Int -> a -> Int
        at test.hs:31:7-45
    Matching instances:
      instance [overlap ok] Count a => Count [a]
        -- Defined at test.hs:7:10
    (The choice depends on the instantiation of `z')
    In the expression: f3 (n - 1) [x]
    In an equation for `f3': f3 n x = f3 (n - 1) [x]

This is with -XOverlappingInstances enabled, and perhaps explains a bit more about the problem. Note the instances only overlap when you try and define 'f3', they do not overlap when defining the existentials, 'f0', 'f1', nor 'f2'. I think the error line (The choice depends on the instantiation of `z') indicates the problem.

Instance selection is by definition dependent only on the type involved. Normally with the case statement examples we can infer the types for each path separately, and we end up with constraints for each 'path' through the code being added to the function type. For the polymorphic recursion the compiler cannot do this because it would require an infinite set of constraints (because we need to know the type of the output of Add to feed into Count, and that depends on the selected instance of Add), and besides you have to supply a signature because it cannot infer the type at all. So you would have to type an infinite list of constraints for each different code path, and type check each of those. So if you unroll, everything works:

f3 x _ = case (x :: Int) of
    0 -> count $ add () ()
    1 -> count $ add [()] [()]
    2 -> count $ add [[()]] [[()]]
    3 -> count $ add [[[()]]] [[[()]]]

Yeah, I think what's happening is that it's skipping past the base case by selecting my new instance, so I guess that does break things. Did I mention that I hate using Haskell type classes for this kind of meta-programming?

Besides Add [a] [a] c matches the instance Add [x] y [z] by unification with x = a, y = [a], [z] = c just fine.

True, but the problem is the next match. Once you perform this substitution, you're left looking for Add x y z, which is Add a [a] z, and we're stuck.

For the polymorphic recursion the compiler cannot do this because it would require an infinite set of constraints

Yes, I agree with this phrasing. With the signature you've specified for f3, it doesn't compile because it's not possible to find an instance that works in that context. If you try to let the compiler infer a signature for f3, it would need to generate infinitely many constraints for a tight enough bound on f3 to make this work.

I still think you could tinker with it to make this case work. Your suggested fix seems a little wonky, since in general an Add x y z constraint shouldn't be able to infer that z is a list (what about Add () () ()?). I think the lesson to draw from this is that Haskell's type class mechanism is a terrible one for doing light weight theorem proving along these lines.

What would you use instead of type classes?

I think the general approach of doing this kind of thing through type annotations is a good idea, but I think the type system should support more customization. It's hard for me to say exactly how it should work in this particular case, because the case is completely contrived and I don't know what the underlying problem is aside from an exercise of type classes. But my guess is that what you want here is symbolics. Something that can easily rearrange '2a = b' into '2(a+1) = b + 2'. That's not well suited to Haskell's strategy of picking the best instance match to the local constraint, committing to it and moving forward.

The particular use is to constrain types. For example constrain a vector to be indexed within its length with no (minimal) runtime checks.

Say we have an array which has a size statically known at compile time (perhaps a 4 vector for 3D card GPU computation) we can limit index lookups to be in range by encoding the size of the vector into the type Vector 3 in Haskell we could represent that by Vector [[[()]]] in my project I will use an integer kind.

If you then have a lookup operation lookup :: Vector t n -> PosLt n -> t you can statically check at compile time that all accesses to this vector are within range. PosLt n is an integer whose type is known to be less than n. This checks static indexing, For runtime indexing we check the static presence of a range check. You need a PosLt n not an Int (which would obviously generate an error). You can provide a function like compare :: Pos -> n -> Either (PosLt n) (PosGe n). Because the only way to get a PosLt n is to use compare this will statically check the index is range checked, and warn of redundant range checks. The type system effectively proves the programming cannot generate code that generates an out of range access at compile time. We can even make this work where the size of the vector is unknown at compile time.

The type level addition above would be used for the concat operation. Haskell's type system can do simple type level arithmetic, but the example of you gave of an algebraic manipulation would be difficult if not impossible.

I will probably use a backtracking solver and primitive type level functions for this. Then use the inferred types plus additional explicit facts (types and implications) to evaluate queries that function like assert statements in the code.

IMO, we should avoid this kind of type-level encoding (as in the PosLt type). We should be able to take a function "lookup :: Vector t -> Nat -> t" and add an assertion to its signature that says that the second parameter should not exceed the length of the first, and this annotation should be in straightforward language and not through phantom types or some such encoding. Such proof obligations should be dischargable at compile-time or deliberately left to run-time.

I agree with the goals, simple readable types, and clear assertions about them, but I think you end up doing the same things in the implementation, so this is really just about how the information is presented to the programmer. If you don't include the vector size in the type, it becomes an associated type rather than a phantom type. I think you run into the same problems as ML has where you can trick the type system into expecting one type whilst providing another. You end up having to add phantom types back in just to keep the type-system safe.

I think you run into the same problems as ML has where you can trick the type system into expecting one type whilst providing another.

I think you can do it right. And I'm not saying I don't want the ability to put length into the vector type. I want the ability to mix and match what's in the type, like perhaps defining an alias type Vec t n = Vector t {.len = n} where the curly brackets specify a refinement type.

The issue I was raising was with the NatLT pattern. I think you'll repeatedly find yourself in a situation where you have a value that's in the desired range, but where you don't have a proof handy of such a fact, and you'll be faced with a decision to either restructure your program to capture this fact by construction or to pay the cost of a run-time check. Also, I consider the calls to that branch function and even NatLT occurrences to be noise that I'd rather not see.

What I'd like to see instead are indicators in the IDE of where undischarged proof obligations are and then have help from the IDE in proving them.

The refinement type is really the same thing, and I like the idea if a 'record' of type-level properties attached to a type. However as I am using extensive type inference the programmer may never directly specify these things, they would be inferred by the compiler from the code path and the assert statements.

Literal values will be lifted straight into type-level values, and the logic solver (prolog style) will be know the rules for inequalities over the built in operators which will be defined both for value-level and type level. After runtime IO a single check would lift the limit to the type level, and that would propagate with the value through the code. All numeric types will carry their range in type form, so potential overflows can be spotted in native arithmetic. There will be a form of subtyping, a narrower range can be accepted in place of a wider one. This should mean no unnecessary checks are required. As function types are polymorphic over type parameters, separate compilation is not a problem.

I don't like tying a language to a particular IDE, but as I am using compositional analysis you could pass a fragment to the compiler and get the errors as XML or JSON to make is easy for IDE developers to integrate.

I'm not going to absolutely require an IDE for my language, but I am designing the language for use with one. I see many cases that have very similar design tradeoffs to the ones here. Since David just mentioned the maxim "explicit is better than implicit" in another thread, I will restate my opinion that the best of both worlds is often implicit selection with explicit feedback. Don't make the programmer spell all of the details out, but let the IDE spell all of the details out for the programmer. The bandwidth of visual feedback to the programmer is vastly greater than the trickle of keystrokes from the programmer.

Implicit selection can be modeled explicitly and extensibly, e.g. in terms of a constraint model or generative grammar. In such a context, I'm all for it. To make effective use of the computing lever, we must automate some of the decision making.

I'm also in favor of rich programmer feedback. Of course, to the extent we model implicit selection programmatically, the feedback about such decisions would need to occur via a more generic vector such as partial evaluation and specialization.

the feedback about such decisions would need to occur via a more generic vector such as partial evaluation and specialization.

I didn't follow that bit. Can you give an example?

If I represent a soft constraint model during the compile-time stage (perhaps using type-level naturals to model 'weights', and type-level computations) then this model is very explicit but the selections it makes are, from the user's POV, implicit.

An IDE attuned to the language in general cannot easily be aware of this specific model or the idioms of its use. But it can still be designed to provide useful feedback about which decisions are made, based on more generic observations. E.g. when there is a type variable specialized on some path through the code based on a global decision of the constraint model, we can render some information about how it was specialized.

Basically, I'm just saying "it's really hard to make a model-aware IDE, but we can still get useful explicit feedback even if implicit selection is modeled explicitly".

So you're saying that implicit selections are programmed explicitly at the meta-level. Yes, I agree with that. The IDE needs to be left extensible because reasonable domain specific implicits can't be baked into the general language.

Extensibility of IDE can also do the job, of course - or at least allow someone else to do it. It isn't entirely clear to me how to approach domain-specific API feedback at the IDE extension level.

Basically, I'm just saying "it's really hard to make a model-aware IDE, but we can still get useful explicit feedback even if implicit selection is modeled explicitly".

Wow, someone should try to write a paper about that.

Write about explicit IDE feedback? I believe you've already done so, or close enough. :D

The problem with Haskell's implementation of type classes for me has always been that it seems to make a closed world assumption. It selects instances on the basis of what it knows about the whole program.

I am not sure but I think this implies that you can break, or modify, a program by adding instances in different modules. I.e., a module B importing A will change B's behavior if you change module A.

Maybe I am wrong but that would break a loose coupling assumption one normally has over modules or code in general. I think it might be a broken system.

Correct me if I'm wrong, but Haskell assumes a closed world approach so it can deal with name overloading correctly. If Haskell didn't support overloading (or it was handled in the IDE), then type classes could work with an open world assumption, right?

I wouldn't know that good. I looked at Typing Haskell in Haskell and it looked they implemented an inferrer with a Prolog style approach of looking at the world. (I stopped reading the report there.)

One manner of looking at it is that their assumption, we should peel off values from types, instead of types from values, is just wrong. Another manner of looking at it is that they do late binding too early within the inferrer, it's broken from that perspective whatever you do; drop the closed world assumption and types rely on values only at runtime.

Not sure though, long time ago.

It depends what you want to do. Values that depend on types are useful for checking static properties at compile time which is what you want in a compiler.

Types that depend on values are only possible with runtime type information, and are useful for dynamic dispatch.

In the former case the compiler proves static properties allowing optimised code to be generated. The latter really just tags data with 'type' information, which is like using a single global datatype:

data Type = I Int | F Float | S String ..

Now you can write case statements and pattern match on the run time type information.

So in summary a static type system is for proving things about a program statically at compile time. If you want dynamic dispatch just use a datatype.

The flame wars have resulted into that languages with dynamic dispatch are now not grouped together with the statically type checked ones?

This is a bit odd. Passing around type dictionaries is pretty close to dynamic dispatch through a different system. Optimizing out RTTI through monomorphization is an old trick too; which is a means of dropping from dynamic dispatch to somewhat static dispatch.

I am more comfortable with calling Java-esque languages statically checked. Doing else results to politics.

I don't really get your point. Datatypes capture the polymorphism of object inheritance heirarchies very well, and support dynamic dispatch and patten matching. Consider an abstract syntax tree:

Data Ast = Var String | Lit String | App Ast Ast

This is equivalent to the following c++

struct Ast {};
struct Var : public Ast {
string const name;
Var(string n) : name(n) {}
};
struct Lit : public Ast {
string const val;
Lit(string v) : val(n) {}
};
struct App : public Ast {
Ast *dom, *cod;
App(Ast *d, Ast, *c) : dom(d), cod(c) {}
};

In c++ you would use the visitor pattern to implement functions that depend on the type of the argument at runtime, in Haskell you just pattern match on the datatype.

Maybe I'm missing something?

I would say that you miss out on late binding with datatypes and that late binding also provides through inheritance, or values implementing interfaces, a manner around the expression problem.

Both interfaces and type classes implement a manner of late binding which gives you an extra abstraction mechanism. You can implement somewhat arbitrary calculations where you defer the actual computation given an unknown value since you know it is associated with a given number of operations.

I find any closed world assumption in the type checker on late binding mechanisms somewhat idiosyncratic; you break the assumption that you're doing computations with respect to an unknown value about which you just happen to know a number of primitive operations.

Of course, you can compile late binding out, or emulate late binding by pairing all values with RTTI. But that's just the Turing tarpit, it isn't a useful observation.

Open-datatypes and open-functions solve these problems without introducing another mechanism. With an open datatype you can do things like:

data AST += Product AST AST

With open functions you can define:

show (Product l r) += ...

It's very difficult to implement open data types and open functions right. There is no right strategy to find the place where a new alternative should be inserted in an open function, it's difficult to check that new alternatives have been added to all open functions when an open data type is extended, and it breaks a rather great deal of invariants assumed while producing code. You'll end up with a pretty slow compiler.

Not worth the effort, doubt it will ever been implemented.

(Apart from that, the expression problem isn't the only problem type classes or interfaces solve.)

There is no right strategy to find the place where a new alternative should be inserted in an open function, it's difficult to check that new alternatives have been added to all open functions when an open data type is extended, and it breaks a rather great deal of invariants assumed while producing code.

Seems like an odd claim. Scala, Haskell and OCaml all admit solutions to the expression problem, and at last MLPolyR and Ur implement type systems that admit direct solutions to the expression problem, instead of the aforementioned indirect solutions.

Not to mention object-oriented statically typed solutions to the expression problem that preserve separate compilation, like open classes.

Or typed, modular, multiple dispatch.