Where clauses on methods

[kjx]

The spec says methods should have where clauses - not just classes and types. (I guess methods have to, since classes and types are "lowered" to methods). What are they, how do they work?

I think where clauses on methods open up great possibilities for libraries, especially when combined with traits. I may have had too much Pinot Noir a couple of days ago, but I think there could be some great options here. I have to look at Martin O'scary's "type classes vs implicits" paper but I have a sneaking suspicion we get something like Haskell type classes for free. Or would if I understood what they are.

Here's an example:

class abstractCollection[E] {
   method sum 
        where E <: type { + Self -> Self }  
        { foldr { a, b -> a + b } } 
   method average 
        where E <: type { + Self -> Self }  
        {  assert size > 0; sum / size } 
}

This is pretty cool: those methods will work if and only if the collection elements can be summed. If we don't give a type parameter, we get Unknown, so the methods will be there and things get checked dynamically. If we give a type without "+" those methods won't be there but other methods that don't have that constraint will be. This doesn't let us add external methods post hoc, but it does make things more flexible.

Furthermore, we can put the methods in a trait:

trait statistics[E]
   method sum 
        where E <: type { + Self -> Self }  
        { foldr { a, b -> a + b } } 
   method average 
        where E <: type { + Self -> Self }  
        {  assert size > 0; sum / size } 
}

And now something a bit weird happens. We can include the trait - but we only get the methods if the element type of the underlying collection supports them! That's different to a where clause on the trait itself:

trait statistics[E]  where E <: type { + Self -> Self }   {
   method sum  { foldr { a, b -> a + b } 
   method average  {  assert size > 0; sum / size } 
}

because it will be an error for that trait to be instantiated without summable arguments.

or we could go one step further, and allow where clauses on e.g. use clauses

class abstractCollection[E] { 
   use statistics[E] where E <: type { + Self -> Self }   
}

(Perhaps when would be better here than where)

This all feels to me, well, rather Haskellian!

[kjx]

Hmm. thinking about the scope of variables in the where clause - can we really make methods "go away" from the types? Don't where clause have to close over method-type-parameters?

method foo[T]  -> Boolean where T <: Stupid { ... } 

this one obviously can't go away.

I wonder if we can say something like: run all the where clauses with method-type-parameters bound to Unknown (hmm, what's Unknown's relationship to <: and :> again? always true?) and in that case if then where clause fails, drop the method out?

[KimBruce]

In the first part, you have a binding problem (at least for more traditional languages. If you introduce a type variable E in a class definition, you normally must put the constraint there, rather than in a method. Could pushing the constraints to later work? I don't know, but would not be surprised if there are some non-obvious problems that could arise!

It certainly would require a much more sophisticated type-checker in a statically typed language. I haven't read Martin's paper so don't know the details.

Finally, is this relevant for a language aimed at novices?

[kjx]

The problem is that we don't have classes. We really don't. (OK technically Tim might argue that we do; they are the generative object constructors, but object constructors are anonymous and nonparametric - the things that are named and parametric are methods).

There is a question as to whether that is appropriate for a language aimed at novices!

But anyway: If we want a class as simple as:

class box[T](initial : T)  where T <: Equality {
     var value : T := initial
     method set(new : T) -> Done { value := new; if (value == initial) then {print "Bing!"} }
     method get -> T { value }
}

it will be expanded into:

method box[T](initial : T) where T <: Equality { 
  object {
     var value : T := initial
     method set(new : T) -> Done { value := new; if (value == initial) then {print "Bing!"} }
     method get -> T { value }
  }
}

so we have to have where clauses on methods. We only really have where clauses on methods. Presumably what they mean is that when the method is called, we run the where clause, and only run the method if the where clause completes normally returning true. That then leaves these interesting possibilities for library design etc.

The big question seems to me to be whether generics are appropriate for a language for novices, and before that whether we can get any kind of (static) type checker going reliably.

[kjx]

earlier I wrote:

run all the where clauses with method-type-parameters bound to Unknown (hmm, what's Unknown's relationship to <: and :> again? always true?) and in that case if then where clause fails, drop the method out?

so this is obviously stupid: because Unknown conforms to everything, the where clause should always pass (unless, well, it is perverse, with negation or something).

A more interesting case might be whether:

class Collection[[E]] where E <: Equality
  {
    method add(e : E) { ... } 
   }

can somehow magically be transformed into something more like

class Collection[[E]] 
  {
    method add(e : (E  & Equality)) { ... } 
   }

The point being that given a Collection of Unknown, an object without Equality would be caught dynamically in the second case, but not in the first. Java does something like this in some cases.

[KimBruce]

A more interesting case might be whether:

class Collection[[E]] where E <: Equality { method add(e : E) { ... } } can somehow magically be transformed into something more like

class Collection[[E]] where E <: Equality { method add(e : (E & Equality)) { ... } } Java does something like this in some cases.

I'm confused. If E <: Equality, why do you need to write E & Equality in the method parameter type? E & Equality is E.

Kim

[KimBruce]

We do need where clauses on methods and your syntax (for classes and methods) is reasonable.

Where clauses won’t be that hard for novices (though it’s a shame to have to throw them in for equality as that forces the introduction earlier). Whether we want to us <: over something a bit less mysterious (e.g., extends) might be a more important issue from the standpoint of usability for novices.

Kim

On Jan 15, 2018, at 1:12 PM, kjx notifications@github.com wrote:

The problem is that we don't have classes. We really don't. (OK technically Tim might argue that we do; they are the generative object constructors, but object constructors are anonymous and nonparametric - the things that are named and parametric are methods).

There is a question as to whether that is appropriate for a language aimed at novices!

But anyway: If we want a class as simple as:

class box[T](initial : T) where T <: Equality { var value : T := initial method set(new : T) -> Done { value := new; if (value == initial) then {print "Bing!"} } method get -> T { value } } it will be expanded into:

method box[T](initial : T) where T <: Equality { object { var value : T := initial method set(new : T) -> Done { value := new; if (value == initial) then {print "Bing!"} } method get -> T { value } } } so we have to have where clauses on methods. We only really have where clauses on methods.

The big question seems to me to be whether generics are appropriate for a language for novices, and before that whether we can get any kind of (static) type checker going reliably.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/146#issuecomment-357790282, or mute the thread https://github.com/notifications/unsubscribe-auth/ABuh-ihUVDRCYc2Ri4xuHvNoWwv3mfZvks5tK79agaJpZM4Rdfc-.

[kjx]

Whether we want to us <: over something a bit less mysterious (e.g., extends) might be a more important issue from the standpoint of usability for novices.

sure- but the catch is we don't have any other syntax like (T extends Q) anywhere...

[kjx]

If E <: Equality, why do you need to write E & Equality in the method parameter type? E & Equality is E.

The issues is - as in Java - what happens dynamically if you add something without equality operators into a collection that needs them, but where you haven't given an explicit element type so E ends up being bound to Unknown by default, and Unknown always matches everything.

That would allow anything to be added into the collection which will then crash when an element doesn't have ==. (You can make the same argument for e.g. sorted collections where the operation required is < or something). Java's generics are rewritten so that the first bound interface is the actual runtime type constraint: so Java will throw an error even with evil casting to stick something into a raw collection that shouldn't fit.

Our design (currently) is that where clauses are general type predicates, so they can't be disassembled or turned into predicates over individual types. Perhaps what somehow needs to happen is that somehow, E should be bound to the actual runtime type of the element (at least until it reaches Unknown) and then that gets checked against all where clauses. Or perhaps the whole thing is crazy. I don't think we've ever had an implementation with where clauses so we've probably no idea.

[kjx]

this is only worth thinking about when we have where clauses