[Grace-core] Type Parameters and parametric type

[Andrew P Black]

I'm sending this to grace-core to keep everyone in the loop, but its really addressed to Tim, Kim, and James, the Type Mavens.

I've deliberately stayed out of most of the types discussions, because I don't know the current literature, but I've found some aspects of the recent discussion on methods with type parameters to be disquieting.

It seems to me that there are two very different situations involved in programming with types.   The first is where there is a type parameter that actually provides information that would not otherwise be there, and changes the behavior of the program.   An obvious example is

	class aList.with<T><a*: T> {
		method contains(a:T)-> Bool { ... }
		method add(a:T) { ... }
		a.do { each:T ->  self.add(a) }
	}

where the type parameter to the list constructor provides information that is not otherwise available (for example, if a is empty or heterogeneous), and changes the behaviour of the body of the method (which generates objects whose method have behaviors observably different form each other).

The second situation is rather different.  It's what the Haskell folks call parametric type and write as forall alpha: alpha ->  f(alpha).    The simplest case is a method like:

	 method id (a:T) -> r:T forall T {
		return r
	}

i.e., a method that simply returns its argument.   The type annotations say that the result has the same type as the argument.  There is no type parameter, and, in my opinion, calling this type parameterization is a bad idea, because the only parameter is a, and it's a value parameter.  It's perhaps better to think of this as a use of dependent type, where the type of the result depends on the type of the argument.

The behavior of the body of the method id does not depend on the value of T: it always does exactly the same thing.  The point of the type annotation is to allow type inference in the context that uses the method id.

I have to admit that the distinction that I've drawn between the body of the method depending on the type parameter in the first case, and not depending on the  type of the parameter in the second, may be flawed.    Perhaps a better distinction is that in the second case, no one would reasonably want to provide a type parameter to id (it would just obscure the program), whereas in the first case, the explicit type parameter clarifies the program.  

The if()then()else() example that we have talked about is a good use for the forall notation:

	method if(c:Bool)then(trueBlock:type{apply()->T})else(falseBlock:type{apply()->T}) : T forall T {
		c.ifTrue(trueBlock)ifFalse(falseBlock)
	}

or maybe

	method if(c:Bool)then(trueBlock:type{apply()->S})else(falseBlock:type{apply()->T}) : S⊓T forall S,T {
		c.ifTrue(trueBlock)ifFalse(falseBlock)
	}

where S⊓T,the meet of S and T, is the type that contains the operations that are common to both S and T.  (Either the lub or the gob, depending on whether one is in the Northern or Southern Hemisphere.) 

I'm not sure how we would write a method like id(), or if()the()else(), in Grace at present.  I'm afraid that it would be:

	 method id <T> (a:T) -> T {
		return r
	}

and 

	method if<T> (c:Bool)then(trueBlock:{apply()->T})else(falseBlock:{apply()->T}) : T {
		c.ifTrue(trueBlock)ifFalse(falseBlock)
	}

I think that this is bogus, because we don't realistically expect anyone to provide T as an argument.  Saying that T is inferred when not supplied, but that it can only be inferred as dynamic, means that type information is always lost when using a method like if()then()else().   The forall notation seems to me to more clearly say that, if the program has type information for the trueBlock and the falseBlock, then it will also have it for the if()then()else().

So, please regard this a proposal for adding something like forall to Grace.    The point of forall is to provide a site for the explicit declaration of what would otherwise be an unbound variable.  It complements the idea of constrained types, for example in

	method negate(a:T) -> T  forall T suchthat T has {¬(x:T)->T} {
		return ¬a
	}

This says that the method negate can be applied to any object that has a ¬ operation.    I'm using a CLU-like notation for matching, and a such that keyword that's not in Grace, because I don't know how to write this in Grace.   (The Grace spec uses a where keyword, which is OK but less suggestive than forall … suchthat … .  It also uses <: instead of matching, which is already annotated as incorrect.)  So you can also regard this as a proposal for concrete syntax for constrained types. 
	
	Andrew

____________________________
Prof. Andrew P. Black
Department of Computer Science
Portland State University
Oregon, USA

http://www.cs.pdx.edu/~black
Telephone: +1 503 725 2411



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/attachments/20131021/9e09a3fe/attachment.html>