Types and annotations should just be requests

[kjx]

Type and annotations are just requests and are requested every time they are accessed. (I think this is thanks to Richard, or else I forget)

That is e.g.:

method foo (x : Number) -> String { x.asString } 

is executed pretty much exactly like:

method foo (x) { 
    if {! Number.match(x)} then {typeError.raise "x isn't a Number" }}
    def rv = x.asString
    if {! String.match(x)} then {typeError.raise "x isn't a String" }}
    rv
}

That is: types (and annotations) are always requested fully late bound. There's no e.g. special stage in object construction the somehow finds types (and annotations) and binds them into some kind of meta-data on methods etc.

An implementation can optimise those requests as possible, and probably should! To support that, we could consider explicit control of side effects i..e strong purity.

[kjx]

I think this works as long as types (in particular) and I guess annotations are more "method-like" rather than "field like".

type Foo = Number | String 

must be closer to

method Foo {Number | String} 

rather than

def Foo = (Number | String)

This is so that e.g. field initialisations can find their types --- if types were defs, then the types may not be initialised before the fields are, or you'd need extra steps in initialisation to build first annotations, then types, then fields/methods, then initialisation...

On reflection, it's also required because types are parametric. Something like this:

type List[T] = Nil | Cons[T] 

needs to mean something like this:

method List[T] = {Nil | Cons[T]}

because defs aren't parametric. Of course this leads straight to infinite loops if they really are just plain methods:

type Cons[T] = interface { 
                            car -> T
                            cdr -> List[T]
                           }

evaluating that as a method gets to a loop PDQ. So types are either method like but special, or perhaps we have 'once' methods (with whatever syntax) and claim types go to once methods...

[ghost]

Type and annotations are just requests and are requested every time they are.

Kernan's parser builds implicit receiver request nodes for both types and annotations. So I imagine that is also what Kernan does; it's definitely how they work in Moth for now.

I thought a little bit about your cyclic example and I don't believe that a types-as-methods implementation of types would cause a problem here. When Cons[T].match(object) is invoked, we need only check that the given object contains the two methods: car->T and cdr -> List[T], right? Unless we needed some kind of "deep type check" (when you would run into the infinite problem), I don't see a problem with the types-as-methods implementation.

[KimBruce]

Recursive types are typically interpreted by co-induction, rather than induction. I.e., try to find an example where the type doesn't work (& if you fail, declare success) rather than proving it does have that type. My (partial) static type-checker works that way. It's pretty standard in the literature.

[kjx]

Yep - where is your checker, btw?

[KimBruce]

There is a type-check branch in mini-grace. The gradualTypesND.grace file is the one I was working on. I tried uploading the most recent version, but it doesn't seem to update (I remain incompetent at using git)!. If it doesn't seem right, I can e-mail it to you or you can tell me how to get it to stick.