[Grace-core] [A Graceful Blog] Comment: "From Lancaster to Portland"
Kim Bruce
kim at cs.pomona.edu
Mon Sep 26 00:10:39 PDT 2011
Two brief comments to add to James'.
1. We are leaning toward allowing singleton types. I.e. if None is an object, then {None} is a type whose only element is None. In particular, it is not a structural type as elt has type {None} at run time iff elt == None.
2. I started writing up something about union types a while ago. While still very incomplete, it at least gives a brief definition of subtyping rules for union types. Because of the restricted subtype rules: U <: S | T iff U <: S or U <: T, the union types are treated similarly to branded types. In particular, if S+T stands for the least supertype of S and T (assuming it exists -- we won't actually have a notation for it in Grace), then S | T <: S + T, but the reverse is generally not true. (Of course it holds in some trivial cases like when S <: T or T <: S.)
What we have in mind is that the only operation available on a union type is the match operation. The real reason for including it is to ensure that we have a match.
I.e., if exp: S | T then a statement of the form
match(exp) {
case{s:S -> stats}
case(t:T -> statt}
}
can guarantee that one of the branches will be taken.
Interestingly, I don't believe we need any uniqueness guarantees. That is, if T <: S then S | T = T | S = S, so an element of type S | T can potentially match both S and T. If we write
match(exp) {
case{s:S -> stats}
case(t:T -> statt}
}
then if T <: S the result will always be to execute "stats".
My original statement about tagged unions was at least mushy (if not incorrect). A better way of saying what I meant is that there is no danger of the usual problems with undiscriminated unions because each object will know its (structural) type and the only way of performing an operation on an element of a union type is either by promoting it to an element of the "sup" type (which likely has very little available to it) or by using the match statement to identify one of the component types that it matches and then use it the appropriate component type.
In particular, you cannot do the kind of evil things that C allows with the union of int and double types where if we have a variable of the union type, you can assign an int and then take it out as a double. Thus, in Grace we manage to avoid type-unsafe operations -- the usual bane to the use of undiscriminated unions.
I've attached my (sketchy) notes on union type.
I hope this makes it a bit clearer why a type like Node | {None}, e.g. where Node represents a node in a singly-linked list, is a perfectly reasonable type that can be used safely in a context where "null" is not an element of every type.
Kim
P.S. If you are going to be at SPLASH, we should be sure to get together to talk. I'm planning on being there through Tuesday afternoon, but leave that evening.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: mainunion.pdf
Type: application/pdf
Size: 62576 bytes
Desc: not available
URL: <https://mailhost.cecs.pdx.edu/mailman/private/grace-core/attachments/20110926/ae2e2f70/attachment-0001.pdf>
-------------- next part --------------
On Sep 25, 2011, at 4:11 AM, James Noble wrote:
> 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
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core
More information about the Grace-core
mailing list