Lambda the Ultimate

Not necessarily - it could also be the type forall a.a.

The problem with that is that modulo side-effects the only thing you can do with it is take the identity. It's narrowing it down to types you know support some operation that's interesting - even if the operation's "take a look at the type tag and dispatch based on that".

It's narrowing it down to types you know support some operation that's interesting [...]

Which even lowly Java supports — I can declare a List<Bar> where Bar is some interface, and then put in objects of any class that supports the interface. This subtyping is usually the feature that I miss most when I occassionally try out Haskell.

...is that no one has come up with a sound type system for OO subtype polymorphism - i.e. a type system that is decidable.

This is similar to writing lisp code where you are determined not to use macros and expect static checks. I'd recommend reading (more) Haskell code to see how a similar problem is solved using Haskell idioms.

Unfortunately I can't think of many examples at the moment, but Oleg's site has a ton of neat code in Haskell and too many other languages (which makes me jealous).

I've read plenty of Haskell code, and I know various ways to solve the problems that I would usually solve with subtyping. I still miss subtyping when programming in Haskell. Are we not allowed to mention features we'd like to see in languages we like?

I also miss it sometimes. A lot of that could be solved with existential types and impredicativity (so that I could have a list of Showable things, for example), but not all of it - record and variant subtyping's useful.

AFAICT, row polymorphism for records and variants is superior (at least in combination with existential types).

Putting impredicativity and row-variable polymorphism in the same language promise to get you quite close to first-class modules. See Daan Leijen's recent work, espeecially Qualified types for MLF.

Impredicativity is nicer than existential types for Philippa's example - you can construct that list of Showable values without needing to inject them into an existential container. I can't see how row-variable polymorphism is at all relevant to that example.

I was rather dismayed recently when I realised that not only does a project of mine fake first class modules in Haskell but that has unavoidable mutually recursive module dependencies - and thus takes some serious effort to pull off in the middle of a 'nice' system.

All I'd done was build a transformer stack for implementations of an API - except the implementations needed to be able to call the 'final' versions of calls.

Incidentally you still need an existential for the type class example to get the right level of polymorphism sadly - it just doesn't have to be faked via the datatype mechanism.

Impredicativity is nicer than existential types

I don't follow. How are existential types interesting without some form of impredicativity in the first place? And how can you construct a list of Showables without at least faking existentials?

I can't see how row-variable polymorphism is at all relevant to that example.

I was commenting on the "record and variant subtyping's useful" part of Philippa's post.

I mean to compare existential types in a predicative and impredicative system. In a predicative system like Haskell you have to make a data type to hide the existential qunatifer if you want a list of existentially typed values. In an impredicative system, you can just work with a list of whatever polymorphic type you like.

I didn't mean that. Nonetheless, "occassionally trying out" sounds quite different now that you put it this way :)

Your example is what is called a discriminated union type (the "discriminated" adjective distinguishes it from the undiscriminated unions of C and C++). Intersection types are different.

Syntactically, intersection types are what you get if you replace the "|" characters in your example with "∧". Semantically, an intersection type is simultaneously a member of more than one type. It can be treated like either type, without a dynamic check. In fancier terminology, the type is inhabited only by those values that belong to each of its subtypes.

I won't hazard to try to give a meaningful example of an intersection type, since I'm at the limit of my understanding in this area.

Perhaps the most intuitive and easy to understand (though not the only useful) is intersection of record types - the values of intersection of A and B have all the fields from both of them (thus, while you intersect extents of A and B, you actually take a union of their features). I believe we already had a discussion of this phenomenon.
[on edit: e.g., Conjunction types]

Know what I wanted to say, just couldn't remember the correct technical term. :-)

Am I correct in thinking that Perl's lists have an intersection type? They are both lists and integers (corresponding to the length of the list).

"Intersection types" refers to a feature of a static type system that lets you define a derived type T by specifying a set of types S. Any value that inhabits every type in S also inhabits T.

For example, if the language used the '&' symbol to intersect types, you could do something like:

class Dog {
   Bark() {}
}
class Cat {
   Meow() {}
}

Run(x : Dog&Cat) {
   x.Bark();
   x.Meow();
}

Run(new Dog()); // -- error
Run(new Cat()); // -- error

class MyWeirdAnimal extends Dog, Cat {}

Run(new MyWeirdAnimal()); // -- OK

A 'new Dog()' value inhabits the type 'Dog'. A 'new Cat()' value inhabits the type 'Cat'. A 'new MyWeirdAnimal()' value inhabits both the 'Dog' and 'Cat' types and therefore inhabits the 'Dog&Cat' type.

Perl's curious that way, in that the notion of scalar versus aggregate context can determine which operation to perform. I tend to think of it as an operator-oriented language with container types, but even that's not entirely accurate.

Maybe it helps to think of evaluating an array in scalar context as calling a method on the array different from the one called by evaluating the array in list context.

Excuse me but the elements of a list of type List(∃a.a) are not of "arbitrary different types"; rather they are all of type ∃a.a.

But this whole thread, frankly, is surely beside the point. The poster does not really want to stick things of different types into a list; he only thinks he does. This is like the guy from that Twilight Zone episode who releases an evil djinni that fulfills all his wishes to the letter, but always in the worst way possible.

The poster thinks he wants to change some language L to L' to allow building such lists because he has some set X of problems which he thinks L' can solve but L can't. And maybe L' can solve them, but only at the cost of creating other problems which are far worse. In fact, he does not only want to solve X in L': he also wants L' to be able to solve all the other problems Y which L was already able to solve: he wants the extension L->L' to be conservative. But it won't be.

What the poster really wants is undoubtedly more dependent on the specific nature of what the problems X are, and in fact might require a number of different techniques rather than one blanket solution.

Languager designers often fall into the trap of thinking that by adding this or that feature it will conservatively address some class of problems because it only involves extending the syntax this way or that. But they fail to see the effect it has on the language as a whole, on its properties, on its semantics.

For example, if you add Type:Type to a language suddenly you get a language where you must drop all pretense of regarding your types as sets, since there is no set which is its own member (by definition). Consequently also "functions" stop being functions, "integers" stop being integers, etc. (*) It is a bit like one of those jokes about screwing in a lightbulb: instead of one guy turning the bulb, he remains stationary while an army rotates the building.

Don't rotate; screw.

(*) These systems can be interesting and worthwhile. But they are not solutions to the problem under the conditions stated.

But this whole thread, frankly, is surely beside the point. The poster does not really want to stick things of different types into a list; he only thinks he does. This is like the guy from that Twilight Zone episode who releases an evil djinni that fulfills all his wishes to the letter, but always in the worst way possible.

Here we have a difference of opinion. In your experience, you may never have come across a problem where you want to process/handle a number of different things - that's fine. However, that doesn't mean that other people haven't.

I have had to solve problems in the past where the solution to the problem was "best"/"cleanest" (from the problems point of view) if there had been a heterogenous list/sequence/stack to place the various "entities" into. Due to the restraints of the programming languages, a considerably more "complicated" solution was developed.

You may well have come up with a different solution - no problem.

The poster thinks he wants to change some language L to L' to allow building such lists because he has some set X of problems which he thinks L' can solve but L can't. And maybe L' can solve them, but only at the cost of creating other problems which are far worse.

Frank, please cite examples of the problems created or give references to papers that discuss examples of these problems. I think that there are those of us who would be interested in seeing what difficulties would actually arise. If they are not obvious, it is then all the more important that they be stated clearly.

In fact, he does not only want to solve X in L': he also wants L' to be able to solve all the other problems Y which L was already able to solve: he wants the extension L->L' to be conservative. But it won't be.

Just as a comment, I have never found any language that suits all problems - I use whatever language is available out of my toolbox that has the particular facilities that I need for the problem at hand. I am, however, interested in some ideas that (from my perspective) have not been adequately investigated. Hence my questions to get a feel for what other people know. Some of the responses have lead to some interesting information.

For example, if you add Type:Type to a language suddenly you get a language where you must drop all pretense of regarding your types as sets, since there is no set which is its own member (by definition).

I have seen this statement made before - a research paper from (I think) about the turn of the century. From my perspective, [Type:Type] is representing the set and is not the set. The research paper (a copy of which I have on one of my backups somewhere) did not seem to differentiate between something acting as a representation and being the thing represented. Your perspective may vary - again not a problem.

For me, each element of the Type Space represents a different Space of Values. Each element of each of these Spaces represents a different value within that space. Hence one of the values of the Type space can and does represent the Type space.

Consequently also "functions" stop being functions, "integers" stop being integers, etc.

[Humour]
Question: What's an integer?
Answer: A can of whole worms that will cause more arguments than is useful - a mathematician represents them by sets (or other things), a prisoner represents them by marks on the cell wall, Scrooge McDuck by the coins in his Vault.
[/Humour]

If the idea that a set can contain a value that represents itself causes the mathematical theorists heartburn, so be it. I personally don't see a problem since we are dealing with representations.

I was trained as an electrical engineer and as a part of the history of engineering, we were required to understand that engineers were using a mathematical technique (algorithm) which worked in practice but could not be proved by mathematicians for over half a century. Till one bright spark jumped laterally a long way and found a solution to why it worked. This pleased the mathematicians and really made no difference to the engineering solution.

Since we are dealing with computational machinery (where where every "thing" being computed is represented by some "thing") and is not a theorectical quantity, a difference from theory will arise.

While all your points have a great deal of truth to them, I have to say that:

Bruce Rennie: If the idea that a set can contain a value that represents itself causes the mathematical theorists heartburn, so be it. I personally don't see a problem since we are dealing with representations.

isn't warranted, because the manner in which we are "dealing" with representations is to manipulate them according to some logic (by the Curry-Howard Isomorphism). Frank's point, or at least my interpretation of it, is that, consciously or otherwise a programmer is making a set of assumptions about the algebraic properties of their code, and that (some of) those assumptions are violated instantaneously, with everything that that implies for the correctness of our code, the moment you introduce something like Type:Type into your language.

In practice, of course, many languages do have the moral equivalent of Type:Type, and people continue to write software in them, but such software traditionally ends up requiring all manner of contortions, some of which fall under the charming-sounding rubric of "design patterns" (many of which simply aren't necessary, or are at least trivial to express, in more expressive languages than Smalltalk, C++, or Java) and others of which simply fall into the category of being unsound, e.g. "instanceof" in Java. If the language in question supports metaprogramming, you now have to worry about non-termination in recursive types. etc.

So while the map isn't the territory, in our domain, the map might best be described as an encoding of the territory—a certain amount of fidelity is, in fact, required for the code to make any sense. To put it in circuit engineering terms, introducing Type:Type has a strong tendency to introduce noise into the system. The signals a user of the language thinks they're sending have a greater likelihood of getting garbled in transmission.

isn't warranted, because the manner in which we are "dealing" with representations is to manipulate them according to some logic (by the Curry-Howard Isomorphism). Frank's point, or at least my interpretation of it, is that, consciously or otherwise a programmer is making a set of assumptions about the algebraic properties of their code, and that (some of) those assumptions are violated instantaneously, with everything that that implies for the correctness of our code, the moment you introduce something like Type:Type into your language.

Agreed - according to some logic. This automatically means that there are some premises that are the basis of the logic that cannot be proved, they are assumed to be true (if you like, the Godel points - if I understand this correctly). If a modification of these premises are used then what is the result? Do some of the logical inconsistancies disappear? This is a question that must be asked and looked at.

If the basis of the logic (and logic is based on ones fundemental beliefs about what is correct) is not allowed to be investigated then one cannot escape from the "boundaries" of the box.

Computers (as we know them) and the "science" behind them have only been in existance for a very short time. So I'll use am example of a logic system that gave rise to a monstrousity - The epicyclic universe. The funny thing was that at the same time it was coming into being an alternative was also being proposed.

Put it as an intuition, but to me it appears that the real fundemantals haven;t been looked at closely enough. I don't have the background (mathematically) to delve deeply into this, but there must be those who are active in the field who can.

Take the above comments for what it is worth (and it may be worth nothing to you).

I have been given enough to start another thread about another subject raised. But I need to formulate the question more clearly.

Today is a good day, I have wood to cut, lawns to mow, a family to spend time with and Jesus to walk with. May much blessing fall upon all of you today.

I have had to solve problems in the past where the solution to the problem was "best"/"cleanest" (from the problems point of view) if there had been a heterogenous list/sequence/stack to place the various "entities" into. Due to the restraints of the programming languages, a considerably more "complicated" solution was developed.

Can you give an example? In my experience, heterogenous collections are almost always a hack/poor-man's-version of a more specific abstraction (object, record, interface, etc.) that a better design (and maybe a better language) would solve more cleanly.

I'd be very interested if you have a specific counter-example.

The simplest example is a print routine. Another is a communications channel between applications (my working background includes communication systems). Both of these, at a more abstract level, process lists/streams of different values. You may disagree and from your perspective that's okay. But from my perspective and those I was working with, the problem required this higher level approach. Because we looked at the problem from this level, we were able to develop a solution that worked where the "experts" were stuck. The tools we had to use were primitive, assembler, cobol, a scripting language called TCL (no relation to the language of that name today). The solution was multi-streamed, multi-user, multi-tasked, multi-machine and it worked. We (myself and another colleague) were able to get the system to work under another OS and communications network very quickly.

Another one of the top of my head that arose so many times over the years is BOM. This one is usually related to databases.

As an apt comment, computer languages are tools and as such, it should be in the hands of the craftsman to choose what tool to use where and when. Whether static/dynamic, typed/untyped, functional/imperative or high-level/low-level.

We are supposed to be craftsmen/craftswomen. Let us develop the "best" tools for the various problem domains that we experience. No two of us will ever have exactly the same set of problems to solve, but we can certainly learn from each other.

I'll leave it here as I need to get out and downtown. Lots of things to do (as previously posted).

Everytime heterogenous lists appear, people talk about print routines. Danvy's Functional unparsing is really cool, typesafe, and implemented without fancy type systems (standard ML, nothing but basic HM types). The technique applies to many other domains.

(edit: fixed link url)

Thank you Carlos for the pointer to the paper. Interesting reading - I'll need to look at it closer. The only problem I have with it, is the fact that it is based on C format strings (reminds of the days when I programmed in Fortran IV and Fortran 10).

From my perspective, C format strings are a kludge and unpleasent way of outputing strings. I do know that other people find them pleasent. Each to his/her own in that regard. The problem I see with them and not addressed by the paper is the printing of "abstract" structures (sequences, lists, communication channels, trees, records, environments, functions, etc) in a simple uniform way, i.e.,

print (sort list)

print (sort table1)

print 12 "This is a string" [ 1 2 34 [ ....] ]

etc.

In addition,

Everytime heterogenous lists appear, people talk about print routines.

it is the one common example of a (system supplied) procedure/function that you can't duplicate by writing your own (with the possible exception of C) - polymorphic and able to process an unlimited number of parameters.

On the whole, it is one reason why I like Icon/UnIcon - they both give you the ability to write your versions of the system supplied functions. You have access to the most of the fundemental features.

Heterogeneous lists tend to be useful when the your dealing with something that isn't well specified. The reasons for a lack of exacting specification are manifold; it could be that you're having to process data from some other poorly specified system; perhaps the requirements for a given portion of ode are not that strict, and flexibility is more important; maybe code that is flexible enough to perform adequately on all manner of input and keep on ticking is more valuable to you than guarantees of getting things right for most cases but is fragile for anything else.

Whatever the reason for not having tight specifications, the result can often end up with heterogeneous lists being a decent answer - sure, if you knew more about exactly what sorts of items you'll ever need to add, or knew exactly how many items you'll need, or any of a number of other things, then you could could likely put together a much cleaner solution, with much better guarantees of correctness, using objects, or records, or union types, or something else; sometimes you don't have that information though.

Sometimes flexibility is of more value in a solution than certainty, sometimes certainty is far more important than flexibility. There's plenty of scope, from dynamic languages, through static types, all the way to formal methods, to cover the needs of different sorts of problems. Can't we just the tool that suits the problem instead of trying to claim that one is better than the other?

Here's why (a weird mix of pseudo-ML and pseudo-Haskell notation, I hope the intention is clear):

type t = 
  [ SomeTypeOfData of int
  | SomeOtherTypeOfData of (int * int)
  | UnknownTypeOfData of string
  ]

func decode :: raw_data_stream -> list t
func decode =
    (try to decode as much as we currently understand)

This trivially lets you add cases as you learn more about the data you're supposed to be processing, and you can get stronger guarantees from the type system(*) than from a type system that allows heterogeneous lists.

(*) Such as full case/match coverage.

The point is that what you have there is something that needs to be taken down, modified, and recompiled, every time a new case that you hadn't yet anticipated comes along. That may well be a good answer for some projects, but other projects have constraints where not having to do that sort of thing is more valuable than stronger type system guarantees.

Think of it like security - sometimes having as many security features in place and locking absolutely everything down is the way to go. Other times secuity just isn't that important, and all those locked down things simply make it impossible for anyone to actually do anything so you sacrificce some security for a little usability. Sometimes there are projects for which correctness is not the most important feature; flexibility is more important. In that case you may well trade off a little type safety for a little flexibility.

I don't see what updating running software has to do with the strictness of the type system. I haven't looked at it too closesly yet, but Acute would seem to provide the necessary language support to make software updates more seamless what with dynamic loading support, type safe distribution, etc.

However, it's worth pointing back at my post here, which copies an example from "Code Reuse Through Polymorphic Variants." The example begins with a simple interpreter for variable substitution, then develops one for the untyped lambda calculus that reuses the variable substitution interpreter, then develops one that does addition and multiplication reusing the variable substitution interpreter, then develops one that combines the lambda calculus and addition and multiplication, all without recompiling any of the earlier definitions. Indeed, they can even be compiled separately. So you can have your polymorphism, static type safety, and extensibility all at the same time, contrary to common belief among those not familiar with the really good statically-typed languages.

Updating a live system without stopping it, however, is indeed a much harder problem. Another poster whose name I can't recall right now has already done me the favor of not having to link to Acute again with respect to those issues. :-)

I think the original poster may be interested in reading about HLists.

"Strong Types for Relational Databases" is also a very good paper which uses HLists to model relational algebra.

I was about to post a question on LtU myself along similar lines of this post: how does one deal with type system in a database environment?

A user may create/alter/remove tables WHILE the database server is running, are statically typed languages still useful in such a scenario? As far as I can tell, the "Types for Relational Databases" paper shows how statically typed tables can be defined in Haskell code by a programmer. How can Haskell's (extended) type system help if one attempted to build a complete database server (a server which receives sql queries, processes its own data, returns results)?

Extensible Union Types are, in my not-so-humble opinion, a better solution to the problem posed by the original poster. I first encountered them in the paper Monad Transformers and Modular Interpreters (Liang, Hudak & Jones; 1995). They are not ideal, but they are much more flexible than Union-Of-Everything types, and not as heavyweight as HLists.

Here's some Haskell code to do what the original posted was asking for:

{-# OPTIONS_GHC -fglasgow-exts #-}
{-# OPTIONS_GHC -fallow-overlapping-instances #-}

{- **************************************************************
   * Extensible Union Types used to print "heterogeneous" lists *
   ************************************************************** -}

import ExtUnion

-- Make Extensible Type Unions instances of the Show class, but only
-- if every member of the union is an instance of Show.
instance (Show head, Show tail) => Show (TypeCons head tail) where
    show (TCHead x)  = show x
    show (TCTail xs) = show xs
instance Show TypeNil where
    show TypeNil = error "show: cannot show TypeNil"

-- Here's a type union.
type PrintableTypeUnion =
      TypeCons Float
    ( TypeCons Int
    ( TypeCons String
    ( TypeCons Bool
               TypeNil
    )))

-- Making ad-hoc extensions to the union is trivial.
type LargerPrintableTypeUnion = TypeCons [Ordering] PrintableTypeUnion

-- Let's see it in action.
main = print ([ toTypeList (1::Int)
              , toTypeList (2.0::Float)
              , toTypeList [LT, EQ, GT]
              , toTypeList "a string"
              , toTypeList True
              ] :: [LargerPrintableTypeUnion])
-- Running main prints:
-- [1,2.0,[LT,EQ,GT],"a string",True]

The code imported from ExtUnion is closely based on code in the aforementioned paper, but yell if you want me to post it here.

Peter McArthur wrote:

main = print ([ toTypeList (1::Int)
              , toTypeList (2.0::Float)
              , toTypeList [LT, EQ, GT]
              , toTypeList "a string"
              , toTypeList True
              ] :: [LargerPrintableTypeUnion])

The OOHaskell paper describes a similar tool called `consEither' --
which creates the similar extensible union type
Either a (Either b ...)
`on the fly'. No prior declarations are needed. Incidentally, such a
union type supports safe downcasting (aka typecase).

Incidentally, by negating HList's extensible records (in the
Curry-Howard sense) we can obtain extensible unions automatically. No
typeclasses are needed and no type declarations. Incidentally, these
extensible unions solve the expression problem for Haskell.

http://www.haskell.org/pipermail/haskell/2006-July/018172.html

The other solution is described in Koji Kagawa's paper `Polymorphic Variants
in Haskell' referenced in the message.

Open data types and open functions which was discussed quite recently on LtU here.

There are at least two fundamental differences between (disjoint) union types and subtyping:

1. Openness vs. closedness. A union type describes all possible alternatives exhaustively. Consequently, a type checker can check that you never forget to handle any of them. With subtyping OTOH the number of alternatives is unlimited - this makes them extensible but also weaker in checking, because you always need catch-all clauses that may accidentally cover unintended cases, especially when you add some later.

2. Subsumption vs. injection. To construct a value of union type you have to explicitly inject it. With subtyping, any value of a subtype implicitly is a value of any supertype. This is more convenient on one hand, but also makes types less precise, because they are only ever exact up to subtyping.

If you meant non-disjoint union types then the story is a bit different, but these are known to be a very bad idea anyway.

BTW, the problem of subtyping (inference) is not undecidable - it just is largely impracticle, and most likely will remain so.

Openness vs. closedness. A union type describes all possible alternatives exhaustively. Consequently, a type checker can check that you never forget to handle any of them. With subtyping OTOH the number of alternatives is unlimited - this makes them extensible but also weaker in checking, because you always need catch-all clauses that may accidentally cover unintended cases, especially when you add some later.

What prevents a compiler from keeping union types open? I do not see it as a problem; a compiler could easily maintain an open slot for extending a union type in released code. The open slot could be optimized away in run time or link time.

Subsumption vs. injection. To construct a value of union type you have to explicitly inject it. With subtyping, any value of a subtype implicitly is a value of any supertype. This is more convenient on one hand, but also makes types less precise, because they are only ever exact up to subtyping.

Again, I see no problem: a compiler could easily provide a typing mechanism where only subtypes of a type are allowed. In this case union types work like C++ templates with constraints: I can pass any subtype of type T, but not T, and a different piece of code will be instantiated according to the type.

You misunderstand. Closedness is not a problem, it's a feature. As I said it allows stronger static checking, and that often is more important than after-the-fact extensibility.

Regarding subsumption I don't understand your comment. What you describe is how subsumption works already. Again, it is an advantage of union types that you do not need subsumption, because that makes the type system more precise.

Subtyping has a different set of advantages, so in short, subtyping and union types simply make different trade-offs.

Closedness is not a problem, it's a feature

If you do not want to add more types to a union type, that is. But what if you do?

As I said it allows stronger static checking, and that often is more important than after-the-fact extensibility

I fail to see how closedness allows for stronger type checking. If a type B is a subtype of type A, then B can fit in any function that requires an A. I do not see how stronger static checking can be.

Subtyping has a different set of advantages, so in short, subtyping and union types simply make different trade-offs.

What I am saying is that subtyping and union types are the same thing, and there shouldn't be any trade-offs/constraints unless explicitely requested.

If you do not want to add more types to a union type, that is. But what if you do?

Then you change the definition and the type checker happily points out every single place you need to adapt. Not so with subtyping (or other open approaches), where code handling existing cases may accidentally(!) subsume new ones without the type checker being able to know and point out. Depending on the application this may or may not be what you want.

If a type B is a subtype of type A, then B can fit in any function that requires an A. I do not see how stronger static checking can be.

By enabling you to say: "Here I want to allow A, and A only!". As soon as you have subtyping, you cannot express that anymore.

What I am saying is that subtyping and union types are the same thing, and there shouldn't be any trade-offs/constraints unless explicitely requested.

What shall I reply to that? I can only repeat that they are not the same thing, and they have different, incompatible advantages. I explained why. You won't change that fact by arguing that one should be turned into the other.

By enabling you to say: "Here I want to allow A, and A only!". As soon as you have subtyping, you cannot express that anymore.

How is that a problem? by using subtyping + constraints, you can achieve just that. For example:

template <class T extends foo> void action(T &a) {
}

In the above, only subtypes of foo are allowed.

I can only repeat that they are not the same thing, and they have different, incompatible advantages. I explained why. You won't change that fact by arguing that one should be turned into the other.

I am not saying that one should be turned into the other. I am saying that they are the same thing! the only difference is that subtyping is open union typing. Don't get caught up in current implementations; think freely. Here is an example:

(* a union type *)
type Foo = Foo1
         | Foo2
         | Foo3

void action(Foo param) { bla bla }

//subtypes
class Foo {
}

class Foo1 extends Foo {
}

class Foo2 extends Foo {
}

class Foo3 extends Foo {
}

template <class T extends Foo> void action(T param) { bla bla}

In both cases, the function 'action' accepts only the 3 elements that are related to Foo: Foo1, Foo2, Foo3.

It seems that subtyping == union types.

In the above, only subtypes of foo are allowed.

You missed the whole point. My example was about being able to express a precise type, i.e. exclude any other type. With subtyping there is no way to exclude subtypes. Of course, that's the whole point of subtyping, but sometimes it is not what you want. See below.

I am saying that they are the same thing!

We are going in circles. I explained why they aren't, and my explanation was not based on any "implementation", but on the standard notions in type theory as well as practical arguments that you want to have both on occasion.

To address your example, with the subtyping formulation you cannot prevent anybody from defining additional subtypes of Foo or FooN somewhere else and call action with them, possibly breaking all its invariants (Philippa gave a good example). So you will never have the same guarantees as with a closed union type.

You examine unions like enums using a case-construct. As the union type is closed, the type checker can verify that all cases are handled. I hope this helps.

If you scroll up a bit, you'll find my crib from "Code Reuse Through Polymorphic Variants," in O'Caml, of an elaboration of three evaluators for a language. The types (var, lambda, expr, and lexpr) are all open thanks to being based on polymorphic variants. The evaluators are all open thanks to relying on open recursion. However, the evaluators are also all annotated to accept only the specific type they evaluate, but to possibly return a subtype—any subtype—of the type that they accept. So as you can see, it's quite possible to restrict a function to taking a specific (union) type and still remain open. And that's just one possible approach; the "Code Reuse Through Polymorphic Variants" web page provides about half a dozen others, with various uses of modules, objects, regular variants, and so on. You might find it interesting.

They are not the same thing, and that's why any attempt to make them the same thing will impose constraints on typical use cases for one or the other. If union types're open, I've no way of knowing that my standard inductive list type's not just been turned into a tree by Moe or Joe "helpfully" adding a data constructor

Branch a (List a) (List a)

. That's a constraint on what I can do with the type system.

You can in fact do subtyping on union types. It turns out to work 'backwards' compared to subtyping on records, but nevertheless has its uses (but see earlier comment about row polymorphism - I've a bad habit of confusing the two because row polymorphism effectively comes with a notion of subtyping).

If you want your union type closed, then the language should allow just that. But in some cases, it may be needed to be open.

A type T1 that is a part of a union type T is a subtype of T, for all practical purposes.

No. I might have more than one data constructor that takes parameters of exactly the same type. There's a link, but it's not as strong as you're claiming.

You're right that open unions have their uses - the classical example would be exceptions. I've advocated them as an option before. They most certainly should not be the default though.

Could you please tone down the claims you make when you think you've spotted a link? You do this regularly, and you get it wrong.

Your notion of first-class types seems to resemble so-called dependent types. There have been a number of experimental languages with dependent types, e.g. Cayenne or Epigram, which emphasize the ability to express all kinds of properties on the type level.

Note however that type theories with unrestricted Type:Type are known to be undecidable, and often otherwise problematic as well (e.g. logical inconsistencies can arise). This is usually circumvented by introducing towers of universes, Type_i, where Type_i:Type_i+1, but not vice versa.

I am a long-time fun of the idea that values are types. See an old comment of mine here:

http://lambda-the-ultimate.org/node/1273#comment-14206

First of all, I have to disagree on subtyping being 'bad' (as in 'XML is bad'). Subtyping is nothing more than classification based on desired properties. In other words, a grouping of values (hence my claim that subtyping equals union types). And with grouping comes reuse. The real problem with subtyping is its implementations: current implementations enforce a cast-in-stone relationship between types which may not always be desirable.

Secondly, I think you can built all types out of three basic types: 0, 1, and a tuple of those. The infinite combinations of 0 and 1 in different configurations can produce infinite types.

For example, a bit is a union type = 0 | 1.
A byte is a tuple of 8 bits.
A short integer is a tuple of 2 bytes.
An integer is a tuple of 2 16-bit words.
A pointer is a tuple of 32 bits.
A linked list is a tuple of two pointers and an integer.
A class is a tuple of its members and a vtable.

So how do you distinguish a pointer from a 32 bit integer? How do you distinguish pointers to bytes from pointers to integers? How do you express the types of functions?

More importantly, how do you express type abstraction? Your examples seem to completely miss the fact that types should express properties (i.e. semantics), not representations (i.e. implementation).

Of course you can encode any kind of information into bit sequences, but that's not news. What's the point of using such a low-level approach for types?

So how do you distinguish a pointer from a 32 bit integer?

You distinguish a pointer from a 32-bit integer by using a strong type definition. For example:

type ptr T = integer 

Then in any function that requires an integer, you can not pass a pointer, but you can do pointer arithmetic because a pointer is just an integer.

If you want pointers without integer properties, then you could
declare a tuple with one member:

type ptr T = {address : integer} 

Then pointer operations can work on the address, but a ptr is not an integer.

More importantly, how do you express type abstraction? Your examples seem to completely miss the fact that types should express properties (i.e. semantics), not representations (i.e. implementation).

Expressing semantics is a different ballgame. I think that the best approach is to have types as functions. Values are functions nevertheless with constant computations. For example, one could declare a positive number like this:

type positive n = n as integer and n > 0

A union type can then be expressed like this:

type foo T = T as foo1 or T as foo2 or T as foo3

Of course you can encode any kind of information into bit sequences, but that's not news. What's the point of using such a low-level approach for types?

The point is flexibility: one can make any type desired, from low level pointers to high level functions. The compiler can stay small (it can even provide only the IR)...if coupled with a powerful macro system that can transform code into basic elements in compile time, then you have a powerful language appropriate for all tasks.

It goes without saying that this is just an idea which might not work in reality :-).

It goes without saying that this is just an idea which might not work in reality :-).

Why not have a go at it yourself? You have lots of ideas and I think developing them in more detail will mature them.

If you need background reading, I'd recommend Benjamin Pierce's
Types and Programming Languages. It has implementations of all type systems that are presented and you can use these as the basis for your own experiments. The book contains enough theory to extend your intuition about the type systems with solid proofs of their power and limitations.

Thanks a lot for the link. I've read parts of the book you mention online, if I recall, and also a couple of other books that I have found lying around in the web.

I have a full time job as a programmer and I do not really have the time to undertake such a big project. Although in my spare time I am trying to write a compiler framework so I can test these ideas.

The answers to these would seem to lie around the already-mentioned dependent types or possibly having Ontic-like semantics.

What is the effect of being able to create new types within the code, in other words having a function that on different invocations returns a new type?

Hmm. Maybe you need to supply code snippets of some examples of what you'd like to do with these first-class types. Are you asking that function to return values of a new type? That doesn't seem possible/desirable in a static language. It seems like only the stuff inside the lexical scope of the original function would be able to use these types. This seems somewhat related to existential types to me.

Another point you'll no doubt want to investigate is why pretty much all languages require types to be declared at the top level.

Also, I think you might be interested in the Omega language, which has higher order, extensible kinds ("kinds" are the types of types).

pretty much all languages require types to be declared at the top level

Well, I have no statistics, but many of the ST languages I'm familiar with allow (at least some) types to be declared at other than the top-level. Take a look at Standard ML, for example.

What is the effect of making Types (or Type Tags) first class citizens of a programming language?

These are actually two different questions, with very different answers.

I'll answer the second question first.

First, think of a type as a classification of data. Then, a type tag is then a piece of data that encodes what the type of another piece of data is. So, the structure of the tag tells you what the type of the object is, and a "dynamically typed value" would be a pair, consisting of a tag and a value of the type indicated by the tag.

So you might have a datatype of tags like:

datatype tag = 
   | IntTag
   | BoolTag
   | PairTag of tag * tag
   | FunTag of tag * tag

Now that you have a datatype of tags (these are richer than usual), you can write an interpretation function that takes a tag, and computes the appropriate type from it.

typeof : tag -> type
typeof IntTag              = int
typeof BoolTag             = bool
typeof PairTag(tag1, tag2) = typeof(tag1) * typeof(tag2)
typeof FunTag(tag1, tag2)  = typeof(tag1) -> typeof(tag2)

Notice that this function takes a piece of data (a tag) as input, and computes a type from it, so we are using a program value at compile-time.

Finally, we can give the type of "dynamic values":

type dynamic_value = (t:tag * typeof(t))

What this type says is that we have a pair, consisting of a tag named t, and a second component whose type is typeof(t).

So a typical program using a dynamic value will project out the type tag, case-analyze it to figure out what type the second component is, and then do something appropriate. This is all sensible and safe from a type-theoretic point of view.

These sorts of definitions are called "dependent types", and are pretty common in theorem proving systems. Limited forms of them form the basis of the ML module system, and for Haskell's guarded algebraic types. Full dependent types will almost certainly start showing up in the next generation of functional language designs, soon to be brought to you by a grad student near you. :)

The answer to your first question, however, about what happens when you make the types themselves (rather than things like type tags) into program values is that many good properties of the type system start to break down, with more properties breaking down the more you can do. Simply adding a type of types to the language is enough to make typechecking undecidable, though it does not let you write programs that dump core. If you can get the type of a value and then case-analyze the type itself, you additionally lose any facility for data abstraction.

They seemed good (very general and basic) questions, which can be hard to answer. I can answer for a Smalltalk-like DT system, but I can't say much about ST languages. Here's a short remark on my ignorance about ST, before I tackle the DT perspective.

I find complexity and/or ambiguity from ST at compile-time hard to tolerate, because it forces me to embrace classes of problems I could arrange to avoid by design. (I suspect avoiding large classes of costs by design instead of facing them head-on is one big distinquishing characteristic among developers.) So for example, I don't understand Haskell beyond surface impressions. I only came close to understanding ML back in 1995, which I had to learn ML well enough to read Andrew Appel's book on compiling continuations. But I soon turned to reading the C and assembler source code for New Jersey ML instead, which told me what I really wanted to know. :-)

Bruce Rennie: What is the effect of making Types (or Type Tags) first class citizens of the programming language?

This happens in some languages like Smalltalk, where a Type is an object of type Class, and every object in the system is associated with a Class. (And each Class has a type which is a Metaclass.)

It makes a language 'reflective' if you can write code asking Type objects questions. If Types survive to runtime (which would make it a lot easier to have code ask questions), and changing these Type objects also changes system behavior, this is part of being 'meta-complete' as well.

A typical thing to ask a Type at runtime is, "What can I do with your instances?" In Smalltalk, dispatching a method to an object amounts to finding a method in the object's class's method table, or in a superclass's method table (which ought to be cached for performance).

Bruce Rennie: What is the effect of being able to create new types within the code, in other words having a function that on different invocations returns a new type?

Mainly it means at runtime you can have all the sorts of changes that might only occur at development time in other more static systems. You'd want to make sure the runtime had good behavior under scaling, in case something extreme happened, like making a new type for every client request sent to a server, as a plausible worst case example.

It makes it hard to reason about what happens with the new types, when trying to predict the limits of behavior at compile time, before the system starts running.

This happens in some languages like Smalltalk, where a Type is an object of type Class, and every object in the system is associated with a Class. (And each Class has a type which is a Metaclass.)

You'll have to forgive me, as I am speaking intuitively rather than from a sound theoretical basis, but I don't believe that a class is the same thing as a type, especially in Smalltalk. I believe that Smalltalk has one type "object" (things that can receive messages) which includes classes. I say this because theres no way to know for sure what class something is. Someone can easily create an object that lies through its teeth, and you probably don't care that it's lying anyway (duck-typing). Having classes to me, in Smalltalk anyway does not equate to first-class types. Smalltalk has only one type that just happens to be very, very flexible.

Aha I see. I sometimes forget that the main point of type-checking is to make sure the program is right, not to play mental games with myself ;).

So, actually, what is the use of types and advanced typing features ?
- Catching errors.
- Function overloading : A single "print" function to remember.
- Optimisation hints for the compiler and precise memory sizing ( for example the bit fields in C, "RANGE" stuff in ADA & VHDL )
- Formal proving

What are the other uses ?

Another use that I'd add to that list is that a type provides a form of compiler checked documentation. Glancing at the type can give quite a bit of information about the function.

Thank you, you are correct. I have just got my copy of the book out and can see my mistake. Dana Scott's name is in a larger font than Joseph Stoy's name on the front cover.

I rushed a little too fast with my typing.

regards and thanks.

The above makes it clear that when it comes to factorial, number 0 is a different type than the rest of the numbers.

datatype number = Zero | Succ of number

val zero = Zero
val one = Succ(Zero)
val two = Succ(Succ(Zero))
val three = Succ(Succ(Succ(Zero)))

fun factorial (Succ x) = (Succ x) * (factorial x)
            | Zero = Succ(Zero)

From this definition, it should be clear that Zero and Succ are constructors of number, and that both constructors yield the same type. More specifically, the set of numbers is defined as the union of zero and all succeeding numbers (ignoring negative integers). The real difference in this case is not that the types are different, but rather that the value of zero does not recursively reference the number type, whereas the succ numbers do. I'd be more inclined to say that the advantage that you cite has more to do with mapping induction directly to the functional recursion over a type.

The case of lists would be similar in recursion:

datatype 'a list = Nil | Cons of 'a * ('a list)

(Also, the subthread on Downcasting in ML is also somewhat related).

O is not strictly a separate type...but it can be thought of as such in the context of a value-based type system...just like nil.

In this case, 0 and all succeeding numbers define the range of values for the type of natural numbers. Dependent types would allow you to have much finer control over the values within a type, but once defined, the stipulated values would all have the same type. Stated differently, the set of natural numbers is [0,1,2,....,n].

It's not that I disagree with your conclusion that functional languages provide a fine facility, it's just that I think you are defining Type a bit loosely. In my opinion, the advantage you are talking about has to do with functional languages directly supporting proof by induction, which naturally lends itself to recursion over a type. As in all cases of proof by induction, you must have a base to start with, and then prove that each succeeding value.

Some languages allow for defining a range type (ADA for example). Zero is a range type by itself. Therefore one can consider factorial (for example) to be defined twice (in other words, be overloaded): one for the range [0] and one for range of [1,inf].

taking such a perspective, you are treading dangerously close to dependent types (a more widely used theme, though, is taking head of cons lists, not factorial).

Not bad by itself, but worth knowing that.

Just as a reminder, one of the relevant LtU threads:

Dependent types: literature, implementations and limitations ?

I think dependent types should be the way forward for programming languages, but I do not see it happening in the next 100 years.

Depends how wide your value of "dependent types" is - the odds of something like GADTs not making their way into the mainstream seems pretty slim to me.

Scheme: The typical Scheme definition of factorial (straight out of SICP) does not use pattern matching. IIRC, Scheme can support pattern matching, but I don't know the language well enough of how it would really differ

(define (factorial n)
  (if (= n 0)
      1
      (* n (factorial (- n 1)))))

Standard ML: SML comes closer to your view of how functions can pattern match on specific values:

fun factorial 0 = 1
  | factorial n = n * (factorial (n-1))

There are a couple of problems with your analysis though. First, there are not two functions here - there is only a single function that has a type (int -> int). You may model in your head that there are two functions being overloaded with two types, but the programming language has no semantics along these lines. The second problem is that the clauses are order dependent. The following ML code will go into an infinite loop:

fun factorial n = n * (factorial (n-1))
  | factorial 0 = 1

Finally, the syntactic form of repeating the function name over the different patterns is really just syntactic sugar for:

fun factorial n =
   case n of
      0 => 1
    | n => n * (factorial (n-1))

which coincidentally corresponds to the form of the Scheme, OCaml, and Haskell code.

OCaml: Caml uses the match construct:

let rec factorial n =
   match n with
      0 -> 1
    | n -> n * (factorial (n - 1))

Haskell: Haskell uses guards to accomplish same:

factorial n | n == 0 = 1
            | otherwise = n * factorial (n - 1)

I think you can write it as 2 seperate functions in Haskell:

factorial 0 = 1
factorial n = n * factorial (n-1)

But I guess it is still order dependent.

I think you can write it as 2 seperate functions in Haskell

Even though the syntax might suggest otherwise, this does not define 2 separate functions. The syntax has the same meaning as the SML example, and similar desugaring rules.

Yes, this is just sugar for case.

Various Haskell derivatives and Haskell-like languages use most-specific pattern matching: Hope is an example.

In OCaml it can also be written everso slightly more succinctly as

let rec factorial = function
0 -> 1
| n -> n * (factorial (n - 1))


...so it doesn't surprise me that there are closer approximations in OCaml and Haskell than I could come up with in short order. I did make sure they compiled first, so at least I know they were legal snippets. I now know a wee bit more about OCaml and Haskell. :-)

I think you could have been a bit more explicit in stating that making the null/non-null distinction a part of the type of value means that a value cannot ever be null when that is not explicitly allowed by its type -- that is, it cannot unexpectedly become null through programmer error on either side of the API. I think that is what most people on that thread were missing.

In my own experience such things did require small "leaps" in understanding before I finally "got" the stronger, more expressive type systems. Being more explicit might help more people make the leap (to the benefit of all :)).

Good observation! thanks.

...that a value cannot ever be null when that is not explicitly allowed by its type

Isn't that the progress property of type safety?

The definition of preservation and progess in
these notes seems pretty standard. Getting null where non-null-ref a is expected is a violation of preservation, unless your type system is so broken you can conclude null : non-null-ref a. Whether it's a violation of progress as well depends on your evalution rules.

Of course, in the context of how Achilleas might have more effective explained non-null reference types he couldn't have assumed his readers would have the formal background in type theory to make this conclusion for themselves.