[Grace-core] [] for types' type parameters (with possible application to classes)

[Kim Bruce]

A very quick reaction.

1) This is not a minor proposal -- at least not the latter parts.  Making types first class has lots of consequences that can be quite difficult to predict up front.  It's my opinion/fear that we face lots of issues with the type system as it is.  We don't want to jump off a cliff into a very rich and confusing type system.  There are many, many things that can (and will) go wrong unless we verify the safety of a type system.

2) A minor question (that may be connected to larger ones) is what is the type of a type definition?  If you write
   def ListOfStrings = List[String] 
then if you are in a statically typed dialect, what is the type of ListOfStrings, and
   def MyList = List
is even worse. 

There are certainly "Kind" systems (paralleling types) that can be used to characterize functions from types to types, but you get into deep water pretty quickly.  Limited expressiveness is your friend if you want a decidable type system and/or to prove type safety.  (The business at the end of using & on type parameters moves us into intersection types, which have never been adapted fully in a major language.)

Having a parallel system of reified types that "represent" types, but are not types, can be safer and might be worth exploring, especially in association with "match".  They can be useful, but not make type checking a bigger problem.

3) I actually like the idea of using [] for type parameters in type definitions, but don't like the idea of using different notations for type parameters for classes, methods, etc.  I'm not sure what the advantage is, and wonder why you'd want to introduce that extra layer of complexity for students of using different notations.  Yes, they are slightly different things, but the parallel notation seems to be more of a help than a hindrance.  Of course, I'm the one who doesn't use [] for accessing elements of lists, etc, so would be happy to get rid of that usage and use [] for all type parameters.  Keep in mind our "odd" syntax rules that require spaces around ">" when used as a comparison, and ban it when used to delimit type parameters.  My students have already run into that issue in my class.  It's easily overcome, but an annoying detail compared to everything else.
--------------

My main concern overall for the proposal is that I don't think we understand the type system as it exists now, and I have serious concerns about how gradual typing will work for us.  Once we get those details worked out we can think of further extensions, but I'm afraid this proposal is more radical than it first appears and will lead us into a world of complexity -- perhaps even worse than Scala's!

Thus I'd encourage exploring similar ideas, but one's that don't require types to be first class.  I understand the need for including some sort of internal representation of types, but hope for one that has few consequences for the language design.  I suspect there is a more conservative proposal embedded in there, but I'd strongly urge caution -- at least until we get a better handle on things.  [As an example of difficulties that may be similar, recall that it is still unknown if wildcard parameters in Java lead to a decidable type system!  There are lots of covariant and contravariant wildness hidden in the bushes.]  Once we fully understand what we have now, we can explore going into the wilds, but I don't think this is the time.
 
Kim



On Nov 13, 2014, at 3:31 PM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:

> Tim and I had a discussion after last week's conference about how
> types should be encoded. There is an issue surrounding type
> parameters: the existence of generic parameters mean that types must
> conceptually be represented (at least dynamically) as methods, which
> isn't ideal. Aliasing and reification are the main issues, and the
> fact that types and other patterns end up with a strange behavioural
> difference. A type accessed from a type definition and a type accessed
> from a type parameter will be conceptually different: one is a method
> request of something, and the other is a local variable access, but
> they're both just accessing a type by its name.
> 
> Instead, we could have (reified) types consistently be objects,
> generally bound to names. Providing them with generic parameters would
> use an ordinary method call. A plausible method to use is the existing
> postcircumfix [] operator from the specification.
> 
> In this case we would fully abandon the use of <> for generic type
> parameters on types. <> would be reserved for declaring and requesting
> methods only. Types would always use []. Static typing would be
> exactly the same as it has been, with just the syntax different.
> 
> Given a type currently written:
>    type List<T> = type { first -> T ... }
> there is be an object in existence representing the type. That object
> is bound to the name "List". It is, itself, a pattern, matching
> List<Unknown> (that is, all lists).
> 
> In this design the object would also have a method [], which would
> specialise the type according to the provided parameters. It would
> return an object representing the newly-instantiated type. The
> implementation of [] would be internal, and memoise the results. So:
>    def ListOfStrings = List[String]
> will create an alias for the instantiated type, while
>    def MyList = List
> will alias the uninstantiated type - these are always genuine object
> references. In both cases, the same object will always be returned.
> Importantly, the "MyList" alias can be specialised in exactly the same
> way, because it is a real object alias.
> 
> All occurrences of parameterised types would use the same syntax:
>    var x : List[String] := ...
>    method lengths<T <: Measurable>(l : List[T]) -> List[Number] { ... }
>    type Listable[T] = type { asList -> List[String] }
> But to request the "lengths" method, you would still use <>:
>    lengths<String>(x)
> In this way types and methods are clearly separated, and types are
> always first-class.
> 
> This also raises some possibilities of higher-kinded types, because
> objects can be passed around and have methods requested of them in the
> ordinary way. That might be useful in some cases. It's unclear whether
> it should be possible to re-specialise the type:
>    def ListOfStringNumbers = ListOfString[Number]
> If it is possible to do, the types should probably be &ed together.
> 
> It is possible that this same approach could be applied to classes, if
> instantiating generic parameters on the class itself is considered
> useful. The class would be an object, able to be specialised by
> requesting its [] method, or instantiated with its constructor method.
> This complicates the encoding, but retains the class as a first-class
> object.
> -Michael
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core