Subtyping

Union types express a subtyping relationship, but I am unclear as to whether typeclasses (i.e. Rust's traits) do?

If a trait B extends another trait A and B reuses the implementations of A, can we assign a trait object that has a bound B to a trait object that has a bound A?

Seems the answer based on prior discussion is yes. But that is a subtyping relationship, which means we would need to deal with covariance on type parameters both when they are trait objects and when they are unions. Correct?

Prior discussion:
#6 (comment)
#1 (comment)
#2 (comment)
#1 (comment)

@keean

@keean wrote:

It will be interesting to see if we still need-trait objects

They are the only way (other than subclassing) I can see to get variance in the polymorphism, i.e. we can assign new types into the trait object (Rust's name for an "existential type" with a typeclass bound) without breaking the invariance of the Array.

The advantage of trait objects compared to subclasses, is that types that can be inserted into a trait object don't have to conform to a pre-existing subclass hierarchy, i.e. it solves some aspect of the Expression Problem¹ but doesn't solve the scenario that unions solve. I am thinking we can view trait objects and unions as complementary in functionality offering different trade-offs on the multi-dimensional design space.

Specifically when we use trait objects for polymorphism, we can add new operations to existing data types (i.e. the trait bound of the trait object), and we can add new data types to existing operations (i.e. implement data types for existing traits), but we can not add new operations to an existing trait object (because the data types have been erased from the static compile-time knowledge of the trait bound type of the reference when assigned to the trait object). And that is the limitation of trait objects that my solution addresses with unions and delayed binding of the union to a trait bound at the function call site. OTOH, unlike unions employed in my solution, trait objects do not require invariant containers in order to add heterogeneous data types to the container because the type of the trait object is invariant. An invariant container is for example a List. Trait objects would also work with an Array which is not an invariant data structure. Apology I am not employing academic terminology such as kinds, rank, F-bounded, etc.. Someone else can do a better job of translating my solution into that terminology.

@shelby3

@shelby3 I am thinking along the same lines. As far as I understand it there is no subtyping. With type classes when we say trait B extends trait A we mean that any implementation of trait B for a type requires there to also be an implementation of trait A, but that is it.

This applies to trait-bounds (type constraints) and trait-objects. Trait-objects are not really a valid type-system concept, these are more correctly called existential types. In haskell if we have an existential data type like this:

data Singleton = forall a. (TraitB a) => Singleton a

The forall a introduces a new scoped type variable, and because its scope is the container, we cannot ever from outside the container know the type of a, but it is constrained to implement trait B and that implies it also must implement trait A. This means we can call any function from the interfaces trait A and trait B on the contents of the container. An alternative way of writing the above (not valid Haskell) is:

data Singleton = Singleton (exists a . (TraitB a) => a)

which is where the term 'existential type' comes from. Generally forall corresponds to the logical concept of any (but may be none), and exists corresponds to the logical concept of some (but at least one).

Agreed no subclassing issue on the type parameters of a typeclass.

@keean

@keean wrote:

I didn't see any mention of type-classes when I looked at Ceylon. It also looks like Ceylon provides classical object inheritance and subtyping, which are both things ZenScript aims to avoid to keep the language small and simple.

Don't we need to be careful about differentiating between subclassing versus subtyping?

ZenScript will have subtyping because it will offer structural unions. An Int is a subtype of an Int|String. ZenScript will not have subclassing.

Ceylon has anonymous structural unions, but it doesn't have typeclasses. <truthful hyperbole>^{Also it has that Jurassic, ossifying, rigor mortise, anti-pattern subclassing paradigm, which will infect with that said virus any program written with Ceylon. Ditto every statically typed language that offers subclassing including Java and Scala (because programmers won't be disciplined enough to not use the subclassing virus in their design patterns).}</truthful hyperbole> 😜

Update:

@naasking wrote:

Ceylon models Java's subtyping via first-class union and intersection types. It's not at all a classical subtyping model.

He replied as quoted above after I wrote the above. Please don't use the word 'subtyping' where you really mean 'subclassing'.

@naasking is apparently unaware of what the programmer can't accomplish with unions and intersections in terms of the Expression Problem if the language does not have the delayed binding of implementation to interface that typeclasses provide.

A typeclass's type parameters can't express genericity that doesn't specialize on implementation. Thus we can't for example parametrize a typeclass trait List<A> to track the type of the elements stored in the list.

Thus we must use a data type to express this:

data List a = Nil | Cons a (List a)

Or add member property names if don't want to be forced to destructure with pattern matching:

data List a = Nil | Cons { head :: a, tail :: (List a) }

In ZenScript perhaps:

data List<A> = Nil | Cons(A, List<A>)

Or perhaps:

interface List<A>
singleton Nil implements List<Never>  // Never is¹ the bottom ⊥ type
sealed class Cons<A>(head: A, tail: List<A>) implements List<A>

Note afaik, Haskell's data type expresses a 'hasA' not an 'isA' subclassing relationship between Cons and List and a can not be heterogeneous because Haskel doesn't have a first-class union type (their global inference doesn't allow for it). If we use this syntax in ZenScript then when instantiating a Cons("string", Cons(1, Nil)) then the type will be inferred List<Number|String>. And if we instantiate first a let x = Cons(1, Nil) its type will be inferred List<Number>. And if we then instantiate Cons("string", x) then the type will be inferred List<Number|String>.

But note even though the above is subtyping, there are no virtual methods on data types, thus no virtual inheritance and no subclassing. Of course any function can input a data type, so that is synonymous with a method, except it isn't virtual dispatch.

Since an eager, CBV language makes Bottom an effect, I have argued the name of the Bottom type should be Never and not Nothing (which appears to be the choice TypeScript made). Bottom is for example the type of functions that never return (terminate). Whereas, in a lazy, CBN language such as Haskell, Bottom becomes a value, so I argue it should be named Nothing and not Never.

Or, with types

data Nil = Nil
data Cons<A, B> = Cons<A, B>
trait List A
impl List Nil
impl<A, B : List<A>> List Cons<A, B>

As a single type with multiple constructors (tagged union):

data List<A> = Nil | Cons<A, List<A>>

I'm still not sure about which keywords we should be using for trait, impl and data.

@keean

@keean wrote:

data Cons<A, B> = Cons<A, B>

data List<A> = Nil | Cons<A, List<A>>

That seems incorrect. It doesn't tell me how to construct an instance of Cons. Mine was correct:

data List<A> = Nil | Cons(A, List<A>)

And we can add member property names if we don't want to be forced to employ pattern matching to destructure:

data List<A> = Nil | Cons(head: A, tail: List<A>)

@keean

@keean wrote:

data Nil = Nil
data Cons<A, B> = Cons<A, B>
trait List A
impl List Nil
impl<A, B : List<A>> List Cons<A, B>

That seems incorrect. I think it should be instead:

data Nil = Nil
data Cons<A> = Cons(A, List<A>)  // Edit: `List` is a typo and should be `Cons` per subsequent discussion
trait List
impl List Nil
impl<A> List Cons<A>

Remember the trait List should know nothing about A if its methods don't specialize on A.

@shelby3 wrote:

A typeclass's type parameters can't express genericity that doesn't specialize on implementation. Thus we can't for example parametrize a typeclass trait List<A> to track the type of the elements stored in the list.

Note I'd prefer to write that:

pluggable List
implement Nil for List
implement Cons<A> for List   // no need to write the type parameters twice per my
                             // proposal¹ that all UPPERCASE names are type parameters

Or much better:

pluggable List
Nil implements List
Cons<A> implements List

I think the last is best because it remains very similar to Java, yet we change the meaning of what is being implemented from interface ('isA' relationship) to pluggable ('hasA' relationship).

Thinking about a typeclass as a pluggable interface seems very intuitive. We can't use Rust's trait because trait has a different meaning in several other languages.

Q: "What is a pluggable API?"
A: "It means that you can replace the implementation."

Remember we both decided that clarity trumps brevity (e.g. implement instead of impl), especially for syntax which is not expression-level (because such declarations won't appear often because most frequently appear in source code are expressions).

Function Syntax #6 (comment)

Not quite :-) some things to discuss. You have given value constructors round brackets, that seems okay to me.

data List<A> = Nil | Cons(head: A, tail: List<A>)

Normally the arguments to cons are positional like function arguments, and deconstructed by pattern matching. You would use record syntax to name them, so either of the following:

data List<A> = Nil | Cons(A, List<A>)
data List<A> = Nil | Cons {head: A, tail: List<A>}

We don't have to stick to that but it's how I was thinking.

This has more problems:

data Nil = Nil
data Cons<A> = Cons(A, List<A>) // list is not a type
trait List
impl List Nil
impl<A> List Cons<A> // cons needs two type parameters

So correcting this:

data Nil = Nil
data Cons<A, B> = Cons(A, B) // constraints on data bad.
trait List<A>
impl List<A> for Nil
impl<B : List<A>> List<A> Cons<A, B>

Note this is still Rust syntax that gives special treatment to the first type class parameter, and I am not sure that is best, but let's have a different topic for that when we have agreed this.

@keean

@keean wrote:

You have given value constructors round brackets, that seems okay to me.

Yeah to differentiate them from type constructors, and because value constructors in the Java-like languages use round brackets (aka parenthetical grouping).

Normally the arguments to Cons are positional like function arguments, and deconstructed by pattern matching. You would use record syntax to name them, so either of the following:

You are repeating what I wrote. I even linked to the Haskell record syntax upthread.

However the following is not naming the members of Cons (rather is only providing their positions and types), and can only be destructured with pattern matching as I already wrote in my prior comment:

data List<A> = Nil | Cons(A, List<A>)

And to stick with the Java-like syntax (and not mixing in Haskell syntax), I would prefer the following which I think will be much more clear to mainstream programmers coming from popular programming languages:

data List<A> = Nil | Cons(head: A, tail: List<A>)

The following is mixing a JavaScript unnamed Object with some new concept of a tag of Cons, which has no analogous concept to people using JavaScript or OOP languages (and our guiding principle is not to introduce unnecessary syntax, i.e. the new concept of a { ... } where we don't need to):

data List<A> = Nil | Cons {head: A, tail: List<A>}

@keean

@keean wrote:

This has more problems:

data Nil = Nil
data Cons<A> = Cons(A, List<A>) // list is not a type
trait List
impl List Nil
impl<A> List Cons<A> // cons needs two type parameters

I had a typo and Cons does not need two type parameters (two would mess up other things):

data Nil = Nil
data Cons<A> = Cons(A, Cons<A>)
trait List
impl List Nil
impl<A> List Cons<A>

The type of the type parameter A in Cons<A> will be subsumed to the GLB of the union of two types used to construct a Cons. I had already explained that as follows.

@shelby3 wrote:

If we use this syntax in ZenScript then when instantiating a Cons("string", Cons(1, Nil)) then the type will be inferred List<Number|String>. And if we instantiate first a let x = Cons(1, Nil) its type will be inferred List<Number>. And if we then instantiate Cons("string", x) then the type will be inferred List<Number|String>.

Note in the above quoted text, I was referring to a data type List not a typeclass List. Refer to that quoted comment for the declaration I employed there (which differs from the List in this comment).

@keean wrote:

So correcting this:

That is still incorrect. You have a type parameter A on typeclass List which I already explained (and you even agreed!) is incorrect as follows.

@shelby3 wrote:

Remember the trait List should know nothing about A if its methods don't specialize on A.

@shelby3 wrote:

A typeclass's type parameters can't express genericity that doesn't specialize on implementation. Thus we can't for example parametrize a typeclass trait List<A> to track the type of the elements stored in the list.

Follow the link in the above quote to see where you had agreed. In fact, you were the one who explained the issue to me. And now it seems you forget what you explained to me.

Actually the above is revealing a deeper issue to me about higher-kinds which I had realized when I woke up this morning. I am preparing to write about that.

The {} have the same use in 'C' for structs, C++ and Java for object definition so they are not new as such.

In C, C++ and Rust we would write:

struct Cons { 
    head : Int, // this syntax is different for C
}

Which we are writing:

data Cons = Cons {
    head : Int
}

Or

data Cons = Cons (
    head : Int
)

I am happy with either, providing the field names are optional, but I wanted to point out that the data statement can be viewed as an extension of struct and object definition.

@shelby3

@shelby3 wrote

I had a typo and Cons does not need two type parameters (two would mess up other things):

Yes it does, what you wrote cannot ever end in a Nil.

@shelby3

@shelby3 this version is correct in Rust syntax:

data Nil = Nil
data Cons<A, B> = Cons(A, B) // constraints on data bad.
trait List<A>
impl List<A> for Nil
impl<B : List<A>> List<A> Cons<A, B>

Cons needs a second type parameter because B can either be another Cons or a Nil which are different types.

The trait List needs a type parameter for the type that in the list, which is not the same as the type which is a member of the class (that is Nil or Cons<A, B>)

When we add Cons to the List type class we need to constrain B to be in the List type class so that you cannot put any random type as the second Cons parameter.

@sighoya

@sighoya Specialisation and scope of instances is a different topic.

True, but I had related it to union types implying the use of subtyping. Maybe another thread is more appropriate.

Edit: so the question is how could you determine which of two Print interfaces to use? All the type system has to do is to check that there is exactly one implementation of Print in scope inside the 'if' statement. So for example:
if (data `implements` Discriminator) { // we know data implements the Discriminator typeclass
  if (data.disc() > 32) {
     using PrintA
     ...
  } else {
    using PrintB
     ....
  }
}
so we can use any value based runtime logic to bring only one of the possible typeclasses into implicit scope.

Hmm, this seems to utilize named instances to disambiguate issues of global coherence.
But the point is, you may don't know all the names of the caller's typeclass instances because the callee is decoupled from the caller over library mechanism.

@sighoya

@sighoya I think the important point to remember is that typeclasses have dynamic scope. So the instance in scope can be determined anywhere further up the call-stack.

This works fine except where the type of a variable is 'Unknown', in which case we must use the type tag or value of the variable to determine the instance to use.

If we consider the two methods of selection I mentioned above: if we guard on a type like 'Int' then we would use the same instance we would use if the type were statically determined to be 'Int'. If we guard on a typeclass like 'implements Print' then we still require that whatever type is dynamically passed resolves to a single instance.

We could summarise this requirement as we require 'global coherence' of typeclasses for in every expression, but we do not require the same resolution in every expression. In Haskell we require global coherence globally, that is wherever you are in a program the typeclass for a given type must resolve to exactly one instance, and it must be the same instance everywhere. What I am suggesting here is global coherence locally, IE there must be exactly one resolution at every point in the program, but the resolution can be different for every point in the program.

@keean

@keean wrote:

I think the important point to remember is that typeclasses have dynamic scope. So the instance in scope can be determined anywhere further up the call-stack.

So you prefer dynamic resolution for trait objects and all the types which has instances associated to the typeclass of the trait object.

If we guard on a typeclass like 'implements Print' then we still require that whatever type is dynamically passed resolves to a single instance.

There is a problem with this view.

object module1
instance Trait for Int

fun()=module2.fun(2:Int)
gun()=module2.gun(2:Int)

object module2
instance Trat for Int

show[S](s:S)requires Show[S] =...
fun(t:Trait)=if(s `implements` Show) show(s)  else ... //what impl is chosen for Show? The one of module1 or module2
gun(t:Trait)=if(s `implements` Show) (i=s:Int;show(i))  else ... //different to fun above?

If you take the instance from module1 for s, then your instance resolution is dynamic, which I may assume you prefer. But what about module2.gun? If you do it likewise, any call of a function with any type which doesn't necessarily have to be typeclass bounded have to include all the dictionaries of the parameter types of the called functions. This would allow to override any called typeclass method in the calle.
For instance:
You want to add numbers: linear(a:Int,x:Int,c:Int)=a*x+b, but the caller of fun provides new implementations of (+) and (*) for Int which may doesn't correspond to addition/multiplication to any means. Now, calling linear doesn't make sense anymore as it cozenage in what it does.

In my eyes, it is better that only trait bounds and trait objects have dynamic resolution implying dynamic resolution in module2.fun, but not once the inner variant data type is visible from the trait object implying no dynamic resolution in module2.gun.

This is the reason I'm against dynamic instance resolution for the variant data types in the union type because the variant data types are visible.

@sighoya

@sighoya Hmm I struggle with examples in Scala, because its a mess, and I don't want to pollute my brain :-)

Instead lets think about simple runtime semantics. We pass dictionaries into functions (as implicit arguments) which is an implementation of typeclasses. This has 'dynamic scope' because the caller can choose which dictionaries to pass in.

We can see this working for all static cases, because if we statically know the types, we know which dictionaries to pass in.

For any function we know the complete list of functions it calls, which means we can always implicitly know the set of required functions for any call. We need this to be inferred, so library functions can pass through dictionaries to callbacks etc.

So given a heterogeneous collection we can calculate at link time the set of dictionaries required by any object put into the collection. This solves one degree of the expression problem because we can add any datatype providing it implements the correct set of typeclasses.

Alternatively we can know at link time the set of types that are put into the heterogeneous collection, in which case we can call any function on the collection that is defined for all types in the collection. This allows us to solve the other side of the expression problem, because we can implement a new function on the collection by providing overloads for all the types in the collection typelist.

Both of these methods work statically and we can imagine combing them, so to solve the expression problem we need to statically know all the types inserted into the list, and all the functions called on the list, which is of course possible to do statically by type inference and typeclass inference.

So this is great, the expression problem is solved, except that we must statically know the whole program. Of course extending this to modular compilation is easy, as we just need to know the list of types that are returned by every function, and the typeclass requirements for every argument. So providing our interface definitions carry sufficient information, there is no problem with modular compilation.

So the only remaining problem is with runtime module loading. Again we can solve this by implementing the correct checks on dynamic loading. If we are loading a module that applies functions to the values in a heterogeneous collection, then the dynamic loader needs to check that the functions typeclasses are implemented for all possible types that can be in the collection (remember we can determine this statically at link time). If the module inserts values into the collection then the dynamic loader needs to check that all typeclasses that are called on collection values are implemented for the types inserted.

To think about this another way, the problems with typeclasses come from the Open World assumption. We can avoid this by moving to a closed world assumption, but the problem is this limits the expression of extensibility. We can recover expression by deferring closing the world until link time by improving our module interface definitions with the extra information outlined above, but this precludes dynamic loading. We can recover dynamic extensibility by having a closed world with extensions. So the world is closed before the dynamic module load and it is closed after. This makes it the responsibility of the dynamic loader to prove the world is closed by checking the interface of the loaded module against the interface/signature type it is being loaded into.

@sighoya

@sighoya Okay, I think I understand your example now, and the answer is, we cannot tell which module will be used, because:

neither module seems to define "show"
we cannot see the call to 'show' to determine the context.
'show' seems to be recursive which must be some kind of error?

What we can say is that we must pass show a dictionary for typeclass 'Show' for the type s in the arguments to the function definition. Which dictionary is passed depends only on the caller, and not the definition of show.

@keean

@keean wrote:

'show' seems to be recursive which must be some kind of error?

Forgot that show was part of the Show interface.

Which dictionary is passed depends only on the caller, and not the definition of show.

Does it hold for both module2.fun and module2.gun with variant data type integer?
Note, both module1 and module2 can have an implementation of Show for Int? Is then the Show implementation used from module1 (the caller) or module 2 (the callee)?

To put it more clearly:
If I add two integers, which instance is chosen for (+)::Num p=>p->p->p?.
The lexical or dynamic one?
If you state: the dynamic one, you never can add two integers because integers are trait objects in your language and by dynamic instance resolution you can't know if there is an instance for Int provided by the caller, you may have an lexical instance for Integer but you would never use this because the caller decides if there is one or not.

@sighoya

@sighoya

dynamic instance resolution you can't know if there is an instance for Int provided by the caller, you may have an lexical instance for Integer but you would never use this because the caller decides if there is one or not.

This doesn't make sense to me. The dictionary for Num is an implicit parameter. so its always dynamically passed from the caller, even in Haskell:

double  :: (Num a) => a -> a 
double x = x + x

The typeclass constraint (trait bound) Num a is implemented by passing a dictionary for Num into double.

The typeclass constraint (trait bound) Num a is implemented by passing a dictionary for Num into double.

This is the ~~static~~generic case, but what about this:
foo::Int->Int->Int
foo x y= x+y //Is this valid?

@sighoya

@sighoya

This is the generic case, but what about this:

Well that's optimised, and not the "real" type:

foo :: (Num Int) => Int -> Int -> Int
foo x y = x + y

This is valid, and foo needs an argument of an implementation of Num for Int...

This is valid, and foo needs an argument of an implementation of Num for Int...

This is a typical question if lexical entities has priority over/under dynamic entities.

To illustrate again the problem:

foo::Int->Int->Int 
foo x y = x+y

is in your language equivalent to:

foo :: (R requires Int[R],Num[R]) -> (S requires Integer[S],Num[S]) -> (T requires Integer[T],Num[T])
foo x y = x+y

So x,y,$returnValue are typeclass objects which may get dictionaries for Num for the types R,S,T from the caller (dynamic scoping).
Another possibility would be to inject the instances from Num for Int from the module declaring foo, in this case all Int Types are not typeclass objects.

What about this?:

foo2::Int->Void
foo2 a= (b::Int=a; fun(b))

Does it become?:

foo2::(T requires Integer[T])->Void
foo2 a = b::(T requires Integer[T])=a; fun(b)

or

foo2::(T requires Integer[T])->Void
foo2 a = b::Int=a; fun(b)

@sighoya

@sighoya
Depends on the requirements of fun. If we assume fun is foo:

foo2:: (Num Int) => Int -> ()
foo2 a = b::Int=a; foo(b

This is true even for:

foo3 :: (Num Int) => ()
foo3 = foo 3

@sighoya

@sighoya Thinking about unifying typeclasses and algebraic effects, we might prefer to write:

foo2 :: Int -> {Num Int} ()
foo2 a = b::Int=a; foo(b)

The reason for this is that effects can be seen as a row-polymorphic monad, so like we write IO a for the IO monad we can write {...} a where the curly brackets are the row. Row polymorphism solves the problem with monads in that they do not compose, but row-polymorphic monads do.

In this way we can also keep the language pure, and encapsulate all state in algebraic effects.

https://overreacted.io/algebraic-effects-for-the-rest-of-us/

What is interesting about this article is that it shows how algebraic effects can remove the 'function colour' from sync/async functions in exactly the same way it can from pure/impure functions.

Navigation Menu

Repository navigation

Subtyping #8

1001 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Subtyping #8

Description

Activity

shelby3 commented on Sep 21, 2016

keean commented on Sep 21, 2016

shelby3 commented on Sep 21, 2016

shelby3 commented on Sep 22, 2016

shelby3 commented on Sep 22, 2016

keean commented on Sep 22, 2016

keean commented on Sep 22, 2016

shelby3 commented on Sep 22, 2016

shelby3 commented on Sep 22, 2016

keean commented on Sep 22, 2016

shelby3 commented on Sep 22, 2016

shelby3 commented on Sep 22, 2016

keean commented on Sep 22, 2016

keean commented on Sep 22, 2016

keean commented on Sep 22, 2016

1001 remaining items

sighoya commented on Jun 30, 2020

keean commented on Jun 30, 2020

sighoya commented on Jun 30, 2020

keean commented on Jun 30, 2020

keean commented on Jun 30, 2020

sighoya commented on Jun 30, 2020

sighoya commented on Jun 30, 2020

keean commented on Jun 30, 2020

sighoya commented on Jun 30, 2020

keean commented on Jun 30, 2020

sighoya commented on Jun 30, 2020

keean commented on Jun 30, 2020

keean commented on Jul 1, 2020

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions