[Grace-core] Type declarations

[Timothy Jones]

On 20/03, Andrew P Black wrote:
> I don't understand this.  If there is no structural type information in a
> branded type, how can you check that I'm telling the truth when I claim that
> an object has a branded type?  Presumably, you want to make sure that the
> interfaces AND the brands match when checking a branded type.

I don't know how much I can say about the paper, but essentially no, there is no
structural information associated with a brand.

> My suggestion for the declaration keyword would be "const" or "manifest", in
> the sense of compile-time constant, used just like we use def right now.   The
> right-hand–side of a const or manifest declaration must be compile-time
> evaluable.  Interfaces are one example of that; your pattern types are
> another, if I understand correctly.

The issue is that the meaning of what is 'statically known' is up in the air due
to the pluggable types. A brand type isn't really a compile-time constant, but
the brand static type checker can track them at compile-time.

> That said, I LIKE using type to mean set of methods and with their types.  I
> believe that it's what type OUGHT to mean, in an OO language.  But the "type
> theorists" don't agree ...

Again, pluggable types mean that pretty much anything can be a 'type', because I
can write a checker that treats it as such. My argument is that the structural
type literal is just a built-in way of constructing one particular form. If we
want to say that the structural forms are the only 'types', and that we have
pluggable 'checkers' instead of pluggable types, then that's okay. We just need
to come up with a reasonable keyword for the declaration, instead of the
literals, because the two are not the same thing.

-- 
Tim