[Grace-core] [A Graceful Blog] Comment: "From Lancaster to Portland"

[James Noble]

Hi John

first - thanks for a clear and detailed email.
This is really helpful in the language design process.

> Thanks. The branding Andrew Black mentions fits into this
> model just fine.

sure - I do think we can get something to work there...

>  (BTW: Number types will HAVE to be branded,
> because otherwise, they will be unimplementable.)

Well, technically we make do with just one number type,
but we would like to allow more...

> Just to remind people: My main worry is about pattern matching
> with gradual typing.  But some of my worries occur even without
> gradual typing.

OK, right...

> OK, here with syntactic errors are a few examples.
> 
> (1) UNION TYPES
> 
> In James' example on the blog, he defines some types:
> 
> 	class Some[T] { v : T ->
> 	  method extract -> [T] {[T]}
> 	}
> 
> 	def None = object { } 
> 
> 	type Option[T] = Some[T] | None
> 
> (Personally, I don't understand the syntax of the extract
> method.  I would expect:
> 	method extract -> T { v }
> but I assume we can all muddle our way through syntax.)

It's a typo & experimental syntax - it should be something like 
    method extract -> Tuple[T] { [v] }

Extract needs to return a tuple (or here, a oneple :-)
so extract works with subtypes...

but we haven't decided on tuple & collection syntax yet
(see the other blog post)

> The first thing that comes to me is that, since James assures me
> that there is no tagging of union types, other than the
> fact that ALL objects are tagged, that the type Option[T]
> is essentially equal to None: The None type permits any object
> (it is the empty structural object type).  Thus anything can be
> passed to something of type Option[T].

Ah. Yes - "type None = { }"  would do just that.

This code was derived I think from Scala originally - so
"None" here is a singleton object type - it will match
*just* that particular empty object.   [[Hmm. orthogonal point:
actually it would match any empty object since we can't
distinguish different "instances" of value objects]]

> This is what I originally asked of the blog and Kim Bruce assured
> me that these union types were NOT set-style union types.
> (And thus Option[T] was NOT identical to None.)  

Option[T]'s not supposed to be identical to None, because
None isn't  the top type...

> But that led me to assume that there is some "inleft" "inright" explicit
> coercion needed to create something of a (tagged) union type
> a la ML.  But James says that's not necessary because everything
> knows its type.

everything knows its "ground" type.  In particular, a Some[T] "instance"
will know it's a Some, and will know what it's "T" is --- although T  
could be "Dynamic". 

> I hear a contradiction here.  If I have something of type Number,
> then can it be passed to something wanting Option[T] ?

Nope.  Option[T] takes either None or Some[T].

if you wrote "OptionPrime[T] = Some[T] | {} "  then yes
anything could go into OptionPrime[T]

> Some might say that the static type system of Grace will require
> me to put in an explicit cast.  But if that cast has no run-time
> significance (i.e. no tagging), then the gradually typed Grace
> will have set-style union types: the kind that generally
> are thought to be a Bad Idea.  

I fear we do have set-style union types: I have some idea why
they are a Bad Idea, but don't know how badly that effects things
when the objects have their types.

Certainly with my current ideal definition of Option[T]:

def None - object { private var i_am_none }   // private var acts a brand and ensures equality...

def Option[T] = T | None 

then the set of objects to which an Option[T]  can refer is 
the set of obejcts to which T can refer, plus the distinguished None object

> And why would a cast be necessary?
> What indeed is the subtyping rule for Union types?

from the current spec (in the repo, not yet on the web)

>> S <: S | T;     T <: S | T 
>> (S' <: S) & (T' <: T) ==> (S' | T')  <: (S | T) 

So "|" isn't purely a structural union - Andrew suggested we call them
"untagged variants".    The point is that a type that implements that
structural interface of "S | T" won't be a subtype of S | T unless it is 
either a subtype of S or of T.   The point is that a two-branch case
that matches one on S, the other on T, will cover S | T.
We could additionally support structural, union types - or not.

> If I recall correctly, Igarashi's design lets A | B be a supertype of A.

yep...

> Hence Option[T] > None > Number, and we have the Bad Idea in typed Grace
> too.

I don't see that in this case because !(None <: Number) 

> (2) ORDER MATTERS

yes it does. 

> At the very least, we would want a compiler that checked that
> a later case wasn't rendered redundant.

except that, I'm pretty sure with structural typing, this must always be a whole program check.

> 
> (3) TESTING Structural Types at run-time
> 
> Structural types are NOT easy to compare.

yep. We're somewhat aware of this. 
Especially Michael who is implementing the compiler...

> If so, do this.  The checks will be VERY expensive.
> And that's even when all the types are declared.

I still have some hope. I think C# *ground* typing 
is decidable and we are considering
restrictions so that e.g. any program will have
a fixed number of class & object declarations,
composed only via generics.  We could (pre)
compute the N^2 structural subtype relations
between the N classes in the program, record 
them explicitly (as if they were Java-style 
"implements" clauses or C#'s "where").

It seems to me the resulting system would be
no worse than C# / CLR is now - or the NextGen
Java proposal would have been.

> With gradual typing, it gets MUCH worse.  Methods may use
> conditions to decide what to return, and so the type of
> an object is actually undecidable at runtime.

sure - but we don't go that far.  Such methods will simply
return the type "Dynamic" - which matches anything, and we 
carry on from there. 

> In the "Blame" papers, Felleisen and others show...

sure - we're aware of that. Our take (currently) is closer
to Igarashi's paper to be presented this year at Splash:
dynamic checks but no blame.  This means we'll catch 
errors - but without blame, won't always be able to 
allocate them properly.  We're hoping the social dynamics
will do this for us: almost all the time, the student's code
will be wrong! 

> This only works if a cast error is fatal.  But if a cast error
> means "OK, not this branch, try the next one", then a cast
> error found late will be impossible to recover from: we chose the
> WRONG branch and have done who-knows-what side-effecting damage
> since the wrong decision

yep, that is possible, especially where type dynamic is concerned.
Again, C# has dynamic and instanceof - but I guess does not make
that much use of them in real code. \

> If we now have some untyped code that declares:
>    class Cowboy {
>      method draw(g) -> { g.shoot(3) }
>    }
> 
> and pass a "cowboy" as a MaybeDrawable to "show", then should it
> be considered a Shape or not?  

As I currently see things, cowboy would have the type 
type CowboyType = { 
  draw ( d : Dynamic ) -> Dynamic 
 } 


Class shape would conform to CowboyType. 
It sees hard indeed to avoid this!

Using much more type inference than we've considered
you could get something like: 

type CowboyTypeInferred = { 
  draw ( d : Dynamic< { shoot(Number) }  ) -> Dynamic 
 } 

which would not match.

> In conclusion: pattern matching should be on types
> with a implicit tagging BEYOND that provided by the objects
> themselves.

Hmm. I'm still not convinced. 

I think this overzealous structural matching is unavoidable,
or rather, avoidable only with branding - and that branding
may take us back towards a hybrid system like Scala or 
Donna Malayeri's Unity.  But that doesn't seem that related
to the variants per se. 

So, I'm still not convinced, yet, that means we have to tag
each variant.  I can see problems with being untagged, notably
things like Option[Option[T]] - with the singleton defintion

type Option[T]  = T | None

so Option[Option[[T]] = Option[ T | None ] 
                                      = (T | None) | None
                                      = T | None = Option[T]

in other words, the set-style variants aren't compositional
(Andrew? pointed this out to me Darmstadt, I think) 

and this is irrespective of structural vs nominal typing,
and gradual vs explicit vs inerred typing 

(it may be possible to get around this by somehow defining
a parameteric None class, so Option[T] = T | None[T]  but I'm
sure there would be other problems...

Anyway: many many thanks for your example and email -

Please don't think - because I at least am not convinced - 
it doesn't mean I'm not taking these concerns seriously,
because I am (indeed I think we all are).

so thanks again for your email!

James