Subtyping and Parametric/Polymorphic Data Types

[digikar99]

Thank you for the paper! I was wondering if you (or anyone passing by this thread) have any thoughts about what implication subtyping (particularly the existence of the "top" type) has for polymorphic data types. Sorry if this is something that can be derived from the work in the paper.

My understanding is that, in standard ML / Haskell or equivalent, it is possible to write Pair<T> to denote a pair of elements of identical type <T>. However, I don't see how this type is any useful in the presence of the "top" type, because if T is the top type, then this would make Pair<T> as a pair of any arbitrary elements. On the other hand, when T is int or nat, then it results in a somewhat useful type as is the case with ML/Haskell.

I am also coming from a Common Lisp background, and here it is also possible to express types corresponding to singleton elements. For instance, the type (eql 5) corresponds to the value 5, and nothing else! And in the above discussion about Pair<T> type, such singleton types can lead to some fairly useless types.

Common Lisp type system is indeed dirty, and I have been wondering about a better typing layer over it. But while Common Lisp makes heavy use of subtyping (in some sense of the term), I'm wondering if I should give up on subtyping due to the above problem, or if there are saner ways to deal with it. So, I'd be happy to know if you have any thoughts on how a data type like Pair<T> of standard ML could be expressed in the presence of subtyping.

[LPTK]

Hi Shubhamkar, thanks for your interest!

My understanding is that, in standard ML / Haskell or equivalent, it is possible to write Pair<T> to denote a pair of elements of identical type <T>. However, I don't see how this type is any useful in the presence of the "top" type, because if T is the top type, then this would make Pair<T> as a pair of any arbitrary elements. On the other hand, when T is int or nat, then it results in a somewhat useful type as is the case with ML/Haskell.

I really don't know what you are getting at. If you're asking for a Pair<int> in simple-sub, you'll get a pair of two integers. The fact that you can also construct a Pair<top> if you want to does not make Pair useless.

Perhaps you mean that traditional unification will make sure that the types of both elements in the pair will be forced to be exactly the same. I'm not sure how that's particularly useful, though.

in the above discussion about Pair<T> type, such singleton types can lead to some fairly useless types.

Sorry, I am not following. Do you have an example?

Common Lisp type system is indeed dirty, and I have been wondering about a better typing layer over it. But while Common Lisp makes heavy use of subtyping (in some sense of the term), I'm wondering if I should give up on subtyping due to the above problem, or if there are saner ways to deal with it. So, I'd be happy to know if you have any thoughts on how a data type like Pair<T> of standard ML could be expressed in the presence of subtyping.

I didn't see a problem, but I can tell you that typing a dynamic language without the ability to leverage subtyping will likely be much harder.

[digikar99]

I really don't know what you are getting at.

Okay, let me try to use a better syntax; apologies for the confusion! In ghci

Prelude> data Pair a = MakePair a a deriving Show
Prelude> MakePair 2 3
MakePair 2 3
Prelude> MakePair 2 "a"

<interactive>:11:10: error:
    • No instance for (Num [Char]) arising from the literal ‘2’
    • In the first argument of ‘MakePair’, namely ‘2’
      In the expression: MakePair 2 "a"
      In an equation for ‘it’: it = MakePair 2 "a"
Prelude> MakePair "a" "b"
MakePair "a" "b"
Prelude> MakePair 'a' 'c'
MakePair 'a' 'c'
Prelude> MakePair 'a' "c"

<interactive>:15:14: error:
    • Couldn't match expected type ‘Char’ with actual type ‘[Char]’
    • In the second argument of ‘MakePair’, namely ‘"c"’
      In the expression: MakePair 'a' "c"
      In an equation for ‘it’: it = MakePair 'a' "c"

So, above, Pair a is a parametric data type, with a type variable a. Here, the data constructor MakePair has a constraint that both its arguments should be of the same type. So, both the arguments to MakePair can be ints, or strings, or chars, so long as both of them are of the same type. Arguments of different types are not allowed: for example, ghci signals an error if the arguments are an int and string, or a string and char, etc.

However, in a system that allows the "top" type, because all the values are of type "top", all pairs of arguments to MakePair are valid arguments. So, the constraint "both its arguments should be of the same type" is rendered useless, and therefore the type Pair a with the type variable a as defined above is not useful.

I certainly do agree with you that the types Pair Top or Pair Int are themselves useful. But I can't think of the role of the type variable a in Pair a. In a system with the "top" type, the constructor for a parametric type Pair a becomes functionally equivalent to the constructor of non-parametric type Pair and so the parameterization with the type variable a seems to add no constraints. I wonder if you have any thoughts about this.

[LPTK]

So, the constraint "both its arguments should be of the same type" is rendered useless

Indeed, there is no such requirement when one has a top type.

and therefore the type Pair a with the type variable a as defined above is not useful.

This is where your argument breaks down. There is no causal relationship between your previous assertion and this one.

I certainly do agree with you that the types Pair Top or Pair Int are themselves useful. But I can't think of the role of the type variable a in Pair a.

How about the swap function? Its type is forall a. Pair a -> Pair a. You pass in a Pair Int and get a Pair Int in return, whose elements you can sum up because they are Ints. Can't do that with an unparameterized Pair Top!

In a system with the "top" type, the constructor for a parametric type Pair a becomes functionally equivalent to the constructor of non-parametric type Pair and so the parameterization with the type variable a seems to add no constraints. I wonder if you have any thoughts about this.

Of course! My thoughts are that this is simply false :^P

[LPTK]

You can play a bit with our SuperOOP web demo to get a feel for such a system:

class Pair[out A](fst: A, snd: A)

fun swap(p) =
  if p is Pair(a, b) then Pair(b, a)

fun sum(p) =
  if p is Pair(a, b) then a + b

sum(swap(Pair(0, 1)))

// sum(swap(Pair(0, "oops")))  // type error

The inferred types are:

class Pair[A](fst: A, snd: A)
fun swap: forall 'A. Pair['A] -> Pair['A]
fun sum: Pair[Int] -> Int
Int

[digikar99]

This is where your argument breaks down. There is no causal relationship between your previous assertion and this one.

Uhm, okay.

How about the swap function? Its type is forall a. Pair a -> Pair a. You pass in a Pair Int and get a Pair Int in return, whose elements you can sum up because they are Ints. Can't do that with an unparameterized Pair Top!

I guess I see your point. Even though the type variable is not useful for the constructor MakePair above, it can be useful for other functions, and especially during type inference.

You can play a bit with our SuperOOP web demo to get a feel for such a system.

MLScript/SuperOOP does look interesting!

My thoughts are that this is simply false :^P

Thank you much :D!

[LPTK]

Yes, the parameterization is essential whenever you want to consume values.

Of course if you only think about constructing values and never using them, you will find most things are useless by definition.

[digikar99]

This helps much! Thank you again :)!