forall in Type Syntax

[apblack]

According to the documentation, the interface of String in standardGrace contains the following method header:

indexOf (pattern:String) ifAbsent (absent:Function0⟦W⟧) -> Number | W

The SmallGrace compiler is actually checking the usage of type parameters, and complains that "The name W has not been declared." (Minigrace still largely ignores type parameters.) I think SmallGrace is right: W needs a defining occurrence. Somewhere we need to say forall W. Where? forall is not (yet) in Grace's syntax.

I suggest:

indexOf (pattern:String) ifAbsent (absent:Function0⟦W⟧) -> Number | W forall W

which is a little weird, because the scope of the forall is not made very explicit. This position is also where we have suggested that we put where clauses. An alternative syntax for forall W might be where W:Type or where W <* Object.

An alternative is to make W a parameter:

indexOf⟦W⟧ (pattern:String) ifAbsent (absent:Function0⟦W⟧) -> Number | W

[KimBruce]

I believe we have syntax for this. It is simply a regular type parameter for a method.

indexOf [[W]] (pattern:String) ifAbsent (absent:Function0⟦W⟧) -> Number | W

A type parameter is treated as a universal quantifier. I personally, would be tempted to move it after the “ifAbsent” part, but I believe we agreed to put it only at the beginning (though I don’t remember why).

Of course we could also use local type inference to allow the programmer to drop the type parameter (as we do for if-then-else expressions), which would allow us to drop the explicit parameter.

By the way, another approach would be to use something like Java’s wild card types (e.g., an existential type), but Java screwed that up so badly, that I’d prefer to stay away from that.

Kim

P.S. I’m so flat out with teaching/hiring/trying to meet a 2/15 deadline for an invited paper, that I’ll be able to comment only occasionally for a while. My apologies.

On Feb 5, 2018, at 11:44 PM, Andrew Black notifications@github.com wrote:

According to the documentation, the interface of String in standardGrace contains the following method header:

indexOf (pattern:String) ifAbsent (absent:Function0⟦W⟧) -> Number | W The SmallGrace compiler is actually checking the usage of type parameters, and complains that "The name W has not been declared." (Minigrace still largely ignores type parameters.) I think SmallGrace is right: W needs a defining occurrence. Somewhere we need to say forall W. Where? forall is not (yet) in Grace's syntax.

I suggest:

indexOf (pattern:String) ifAbsent (absent:Function0⟦W⟧) -> Number | W forall W which is a little weird, because the scope of the forall is not made very explicit. This position is also where we have suggested that we put where clauses. An alternative syntax for forall W might be where W:Type or where W <* Object.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/156, or mute the thread https://github.com/notifications/unsubscribe-auth/ABuh-qp81M9P66S1AdYrNeLLMcmAqipYks5tSALhgaJpZM4R6n2n.

[kjx]

Of course we could also use local type inference to allow the programmer to drop the type parameter (as we do for if-then-else expressions), which would allow us to drop the explicit parameter.

Aye there's the rub. A static checker can infer and check types within a module - or even across modules, although I don't know if anyone's ever got that working yet - but what it can't do is populate the dynamic type parameters at runtime.

[apblack]

I think that I'm saying the same as @kjx here: a type parameter is not the same as a quantifier.

When I wrote forall W I intended that the type of the parameter absent be used to determine the type of the result of the method. Making W a type parameter means that the client has to state the type explicitly, and if they do not, then it is Unknown. This is not the same thing at all.

[apblack]

I don't see what this has to do with inference, except of the most trivial kind. If there is no type associated with the argument supplied for absent, then its type will be Unknown, and the type of the whole indexOf(pattern) ifAbsent (absent) request will be Number | Unknown. But if the absent block is something like

{ 0 }

then the result type will be Number, without the client having to type

myString.indexOf[[Number]] (pattern) ifAbsent {0}

I suppose that this requires "inferring" that the type of 0 is Number, but I think that that kind of trivial inference is not typically what one means by type inference. Not that I know anything about types.

Hence, I repeat my claim that a type parameter is not the same as a quantifier, and that what this example really needs is a quantifier, not a type parameter.

[KimBruce]

[Not sure whether I should have opened a new issue for this, but for now I'll just add to this discussion]

As far as I can see, we have not yet identified a syntax for type constraints. (There is a stub in the Language spec in the section "Type Parameters".) Here is a proposal:

class className[[T1,...,Tn]] (a:Tp,...) -> Tpr where
        T1 extends TpExp1, ..., Tn extends TpExpn {
      ... // class body ...
}

Method syntax would be exactly the same, e.g.,

method m[[T1,...,Tn]] (a:Tp,...) -> Tpr where
        T1 extends TpExp1, ..., Tn extends TpExpn {
      ... // method body ...
}

We could have similar syntax for type constraints on types, though we technically don't need constraints on type variables in type definitions (and the syntax would be slightly messier), so I'd just as soon leave out those constraints.

Note that this is a very general syntax that allows mutually recursive constraints on types. Interestingly, it is no harder to do mutually recursive constraints than single ones as you just need to check constraints when the type variables are instantiated. Note that each type variable can appear at most once to the left of an "extends". If a type variable does not occur to the left of an "extends" then it is considered unconstrained.

The name "where" is already a reserved word. We would need to add "extends". We could instead use a new combination of symbols, e.g. <# or <:, but I think the intended semantics is clearer with "extends". Notice that this has no impact on whether or how we support Self (the type of self).

[KimBruce]

Just realized that of course we need constrained types as the types of methods (and hence classes). if have in class c generating objects of type U

method m[[T1,...,Tn]] (a:Tp,...) -> Tpr where
        T1 extends TpExp1, ..., Tn extends TpExp {...}

then the interface will have

type U = {
   ...
   m[[T1,...,Tn]] (a:Tp,...) -> Tpr where
        T1 extends TpExp1, ..., Tn extends TpExp

[apblack]

I didn't get any support for adding forall A rather than making A a parameter, so I'm dropping that proposal for now.

@KimBruce seems to have morphed this issue into a discussion of the where syntax. He proposes a new syntactic concept — a keyword denoting a binary operation. I think that we don't need that, and should use infix operators, which are already in the syntax. Specifically, we should use <: and :> for subtyping, and <* and *>for matching, the latter requiring that Self correspond to Self.

[KimBruce]

I can live with that. I suspect we should have both subtyping and matching as that will be confusing for novices. Because adding matching will require exact types (for contravariant occurrences of Self), I'd suggest just using subtyping for now and restricting uses of Self to covariant positions.

[apblack]

I just changed the title to indicate more clearly what this issue is about.

Here are some more motivating examples:

forall T: pick(source:Collection⟦T⟧) → T 
// top-level method that picks an arbitrary element out of source

forall T forall F: if(cond:Boolean) then (trueBlock: Block0⟦T⟧) else (falseBlock:Block0⟦F⟧) → T | F
// top-level method for conditional application of a block

type Collection⟦T⟧ = interface {
    forall U: map (f:Function1⟦T, U⟧) → Collection⟦U⟧
    //  Collection⟦T⟧ has a map method, whose result type depends on the type of f
   ...
}

I don't see how the methods can be typed without forall, or something equivalent, being available to introduce what are universally-quantified type variables.

The syntax is not important: we could use where-clauses with trivial bounds to provide the same semantics:

pick(source:Collection⟦T⟧) → T where T <: Object
// top-level method that picks an arbitrary element out of source

which actually means ∀ T such that T <: Object.

What I'm looking for here is either agreement that we need some way to introduce universally-quantified type variables, or an explanation of how we give types to these examples without such variables. Note that

if⟦T,F⟧(cond:Boolean) then (trueBlock: Block0⟦T⟧) else (falseBlock:Block0⟦F⟧) → T | F

is not the same thing at all, because it requires the programmer to provide the arguments corresponding to T and F explicitly; if they are omitted, these arguments are treated as Unknown, and consequently the result type of every conditional expression is Unknown.

Note that in the TypeNSemantics paper, the type-checking rule Cond (which assumes that if(_)then(_)else(_) is built-in rather than provided as a method) already requires the type-checker to do exactly the same type inference as my suggested forall syntax. The difference is that without forall, such constructs cannot be defined by the programmer. As I hope my examples have shown, they need to be programmer-definable.

[KimBruce]

I'm not sure I'm understanding the problem, but maybe I'm missing the oint. We have such a notation

pick[T] → T // top-level method that picks an arbitrary element out of source

This specifies a method that takes a type parameter T and an element of Collection[[t]] and returns an element of type T. We write the specification in an object type just as written above. In the types and semantics paper, we would write it as pick: forall T. (Collection[[t]] -> T)

In your third example, we do indeed write:

type Collection⟦T⟧ = interface { map[[U]] (f:Function1⟦T, U⟧) → Collection⟦U⟧ // Collection⟦T⟧ has a map method, whose result type depends on the type of f

This is translated in the theoretical language as

typeConstructor Collection = TFunc(T). interface {...}

I labeled it as a typeConstructor rather than a type as you only get a type after you apply it to some T. If we allowed the user to write type functions in that way we'd have to introduce the "constructor" keyword. However, we force them to write it the first way (with type) and we can translate it at parse time into an abstract tree for a type constructor

Did I misunderstand this issue?

Kim

... }

On Mon, Mar 6, 2023 at 10:55 PM Andrew Black @.***> wrote:

I just changed the title to indicate more clearly what this issue is about.

Here are some more motivating examples:

forall T: pick(source:Collection⟦T⟧) → T // top-level method that picks an arbitrary element out of source

forall T forall F: if(cond:Boolean) then (trueBlock: Block0⟦T⟧) else (falseBlock:Block0⟦F⟧) → T | F // top-level method for conditional application of a block

type Collection⟦T⟧ = interface { forall U: map (f:Function1⟦T, U⟧) → Collection⟦U⟧ // Collection⟦T⟧ has a map method, whose result type depends on the type of f ... }

I don't see how the methods can be typed without forall, or something equivalent, being available to introduce what are universally-quantified type variables.

The syntax is not important: we could use where-clauses with trivial bounds to provide the same semantics:

pick(source:Collection⟦T⟧) → T where T <: Object // top-level method that picks an arbitrary element out of source

which actually means ∀ T such that T <: Object.

What I'm looking for here is either agreement that we need some way to introduce universally-quantified type variables, or an explanation of how we give types to these examples without such variables. Note that

if⟦T,F⟧(cond:Boolean) then (trueBlock: Block0⟦T⟧) else (falseBlock:Block0⟦F⟧) → T | F

is not the same thing at all, because it requires the programmer to provide the arguments corresponding to T and F explicitly; if they are omitted, these arguments are treated as Unknown, and consequently the result type of every conditional expression is Unknown.

Note that in the TypeNSemantics paper, the type-checking rule Cond (which assumes that if()then()else(_) is built-in rather than provided as a method) already requires the type-checker to do exactly the same type inference as my suggested forall syntax. The difference is that without forall, such constructs cannot be defined by the programmer. As I hope my examples have shown, they need to be programmer-definable.

— Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/156#issuecomment-1457638912, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAN2D6SROP4CGRWSZJZTDIDW23LUXANCNFSM4EPKPWTQ . You are receiving this because you were mentioned.Message ID: @.***>

-- Prof. Kim Bruce Computer Science Pomona College

[apblack]

@KimBruce , I think that you have understood this pretty well. In your types and semantics paper, you write

pick: forall T. (Collection⟦T⟧) → T

which says that pick is a method with a single parameter that is a collection of any element type, and that it returns an element of that type.

My point is that we have no way to write this in Grace. We can indeed write, as you suggest,

pick ⟦T⟧ (source:Collection⟦T⟧) → T

but that pick method has two parameters, not one. We have to provide an extra argument on every request if we want the result type to be T and not Unknown.

What I'm asking for is a way to directly write the single-parameter form of pick in Grace.

[KimBruce]

I assume you would not be happy with something like:

pick ⟦T⟧ → Block1[[Collection⟦T⟧,T]]

We can't have a method returning a method, but we can have it returning a function (or object if we wanted to encode it that way).

Otherwise, I don't know how to do that without moving to an implicit type system like Haskell or ML. I believe there would have to be some way of inferring the universal quantification (which is explicit currently in Grace). I personally don't have a problem writing in type parameters, but can imagine some limited inference of the sort found in Java.

On Tue, Mar 7, 2023 at 10:57 PM Andrew Black @.***> wrote:

@KimBruce https://github.com/KimBruce , I think that you have understood this pretty well. In your types and semantics paper, you write

pick: forall T. (Collection⟦T⟧) → T

which says that pick is a method with a single parameter that is a collection of any element type, and that it returns an element of that type.

My point is that we have no way to write this in Grace. We can indeed write, as you suggest,

pick ⟦T⟧ (source:Collection⟦T⟧) → T

but that pick method has two parameters, not one. We have to provide an extra argument on every request if we want the result type to be T and not Unknown.

What I'm asking for is a way to directly write the single-parameter form of pick in Grace.

— Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/156#issuecomment-1459632336, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAN2D6USKMSZH6WHFKNANVLW3AUW5ANCNFSM4EPKPWTQ . You are receiving this because you were mentioned.Message ID: @.***>

-- Prof. Kim Bruce Computer Science Pomona College

[apblack]

Right, I would not be happy with explicitly parameterizing a method.

I don't see the problem. You write "I don't know how to do that without moving to an implicit type system like Haskell or ML.", but your type system already has the feature that we need. The problem is that the language doesn't have a way of writing what the type formalism can already express.

In this example, the type system already knows the type of the argument to pick (Collection⟦T⟧). So why is it a problem to deduce that the result is of type T?

[apblack]

The lack of resolution of this issue is a problem. It is stopping me from writing some of the definitions that ought to be in the standard dialect. Because there was no static type-checker, and because minigrace's dynamic type-checker ignored parameter and result types, not being able to write the types correctly has not been a problem until now.

However, as I try to get a static type checker working, and to improve the dynamic checker to go more than one level deep, it's important that we can write correct type definitions for our standard library; if(_)then(_)else(_) is the paradigmatic example:

    if (cond:Boolean) then (trueClause:U) else (falseClause:W) → U | W  

The definition of type Type⟦T⟧ is also problematic, because of that type parameter; Type⟦T⟧ contains signatures like

type Type⟦T] = interface {
        ... 
        & (other:Type⟦U⟧) → Type⟦T&U⟧    // answers the join (Self & other)
        | (other:Type⟦U⟧) → Type⟦T|U⟧    // answers the variant type (Self | other)
        - (other:Type⟦U⟧) → Type⟦T-U⟧    // answers the type that is like Self
                                        // but excludes the methods of other
        ...
}

In both of these snippets, U and W are identifiers that have no defining occurrence; they are universally quantified, separately for each method signature.

I can see three possible resolutions:

1. Add a forall declarator. The difficulty here is syntactic: where do we write forall U so that the scope of U is clear?
2. (Mis-)use the where syntax. We could allow where clauses at the end of a signature, and say that otherwise undeclared identifiers U that are constrained by where U :< Object are implicitly declared and universally quantified. (As I write this, I'm tempted to say that this is an ugly cop-out.)
3. Do the Haskell thing, and have a "prime" convention where writing a' implicitly declares a universally-quantified type that we pronounce "alpha", just to show that we can keep-up with the Greek Squad.

Maybe there are other solutions?

[KimBruce]

One thing we agreed on early on is that we would only use constructs that were available in multiple other languages. I don't know another language with a forall construct, so am wary about adding that.

The obvious (but inelegant) solution is just to put in the type parameters:

if[[U,W]] (cond:Boolean) then (trueClause:U) else (falseClause:W) → U | W

The only difficulty with this is the user must always put in the type arguments when using conditionals and people would hate that. Because if-then-else is part of the core language, we can write a custom rule for it:

C,E |– cond: Boolean, C, E|– trueClause: U C,E |– falseClause: V

––––––––––––––––––––––––––––––––––––––––––––––––––––––

if (cond) then trueClause else (falseClause): U | W

No type parameters appear in the rule. U and V are derived by the type-checker and hence don't need to be instantiated.

Now I'm not sure what is going on with the Type[[T]] interface. We didn't need the type parameter T when we were writing the type checker.

I have a feeling that you are working one level of abstraction higher than you should be. If S and T are types, then when we form S & T we can provide methods that provide the info we need for type-checking (e.g., what methods are availble to us and how we cna do subtyping).. Working with something like TYPE:TYPE is a sure way of walking off a cliff into very undecidable code.

Is there more that you can tell me to convince me this is necessary? Also, are there other languages that do this kind of thing. If not, why don't they need it?

Kim

On Fri, Mar 17, 2023 at 11:15 AM Andrew Black @.***> wrote:

The lack of resolution of this issue is a problem. It is stopping me from writing some of the definitions that ought to be in the standard dialect. Because there was no static type-checker, and because minigrace's dynamic type-checker ignored parameter and result types, not being able to write the types correctly has not been a problem until now.

However, as I try to get a static type checker working, and to improve the dynamic checker to go more than one level deep, it's important that we can write correct type definitions for our standard library; if()then()else(_) is the paradigmatic example:

if (cond:Boolean) then (trueClause:U) else (falseClause:W) → U | W

The definition of type Type⟦T⟧ is also problematic, because of that type parameter; Type⟦T⟧ contains signatures like

type Type⟦T] = interface { ... & (other:Type⟦U⟧) → Type⟦T&U⟧ // answers the join (Self & other) | (other:Type⟦U⟧) → Type⟦T|U⟧ // answers the variant type (Self | other)

• (other:Type⟦U⟧) → Type⟦T-U⟧ // answers the type that is like Self // but excludes the methods of other ... }

In both of these snippets, U and W are identifiers that have no defining occurrence; they are universally quantified, separately for each method signature.

I can see three possible resolutions:

1. Add a forall declarator. The difficulty here is syntactic: where do we write forall U so that the scope of U is clear?
2. (Mis-)use the where syntax. We could allow where clauses at the end of a signature, and say that otherwise undeclared identifiers U that are constrained by where U :< Object are implicitly declared and universally quantified. (As I write this, I'm tempted to say that this is an ugly cop-out.)
3. Do the Haskell thing, and have a "prime" convention where writing a' implicitly declares a universally-quantified type that we pronounce "alpha", just to show that we can keep-up with the Greek Squad.

Maybe there are other solutions?

— Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/156#issuecomment-1474228225, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAN2D6VUVPNPVFGODT4DMADW4SS4JANCNFSM4EPKPWTQ . You are receiving this because you were mentioned.Message ID: @.***>

-- Prof. Kim Bruce Computer Science Pomona College

[kjx]

Java, C#, Scala, and of course every functional language based on type inference supports just "this kind of thing"

Where Grace (so far) is different is that we do almost* no type inference.

I mean given:

method a -> A {...}
method b(a: A) -> B {...}
method c(b: A) -> C {...}

typchecking something like this requires something that's not that far from "type inference"

def x : C := c( b( a ) ):

[kjx]

A thought - get the type checker going with explicit parameters first - and then work out how to what to do next?

at least that would give something within which to experiment?

could we steal something?

rewriting one or both of these in Grace would be an interesting exercise, would tell us things about AST & typechecker designs, and would probably even let us generate a paper...

https://munksgaard.me/toyml/typechecker.html

http://gallium.inria.fr/~fpottier/X/INF564/html/

https://mukulrathi.com/create-your-own-programming-language/intro-to-type-checking/

[KimBruce]

I agree with James. Also keep the special case for if-then-else so you don't have to write down type parameters for every conditional (you could do the same for match). The type inference I'm aware of in Java (though I haven't looked at it in a while) is very local (e.g. use the type of an initial value to infer the type of a variable/constant). Pushing beyond that would be interesting but likely quite challenging. However, for now, let's get a working type checker without too many innovations (I'm still worried about variants and intersection types more than type inference).

On Mon, Mar 20, 2023 at 12:28 AM kjx @.***> wrote:

A thought - get the type checker going with explicit parameters first - and then work out how to what to do next?

at least that would give something within which to experiment?

could we steal something?

rewriting one or both of these in Grace would be an interesting exercise, would tell us things about AST & typechecker designs, and would probably even let us generate a paper...

https://munksgaard.me/toyml/typechecker.html

http://gallium.inria.fr/~fpottier/X/INF564/html/

https://mukulrathi.com/create-your-own-programming-language/intro-to-type-checking/

— Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/156#issuecomment-1475743618, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAN2D6XQNY325P5U5DQS7OLW5ABIVANCNFSM4EPKPWTQ . You are receiving this because you were mentioned.Message ID: @.***>

-- Prof. Kim Bruce Computer Science Pomona College

[apblack]

About a month ago I did get the type-checker implemented by one of Kim’s students working again, after a fashion. The problem was that it did not have definitions for basic types like Boolean and Number … because it was ignoring imports and dialects. So I started fixing up the definitions of the types that are indeed now part of the standard dialect, as they should be.

The problem is that Boolean has methods ifTrue(_), etc., whose signatures I cannot write. Yes, I could instead define ifTrue as if it had a type parameter, but since that parameter is always omitted, it will always be Unknown, as will the result type. So all type checks will pass. I suppose one could supply actual type arguments, just for tests.

I was hoping to do better. This is the first time that I’ve found myself limited by the expressive power of Grace.

As for other languages that do this sort of thing: add Emerald and Haskell. Emerald has an explicit forall declarator, although I think that it can be omitted if there is also a where. Haskell uses the “dashed-variable convention”, in which lower-case type variables with a ‘, like a’, are treated as being universally quantified.

It’s also true that minigrace currently has if-then-else and match-case built into the parser. True, but completely irrelevant to this language design issue. It’s on my list of things to fix.