Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

forall in Type Syntax #156

Open
apblack opened this issue Feb 6, 2018 · 19 comments
Open

forall in Type Syntax #156

apblack opened this issue Feb 6, 2018 · 19 comments

Comments

@apblack
Copy link
Contributor

apblack commented Feb 6, 2018

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
Copy link
Contributor

KimBruce commented Feb 6, 2018 via email

@kjx
Copy link
Contributor

kjx commented Feb 6, 2018

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
Copy link
Contributor Author

apblack commented Feb 7, 2018

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
Copy link
Contributor Author

apblack commented Mar 1, 2018

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
Copy link
Contributor

[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
Copy link
Contributor

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
Copy link
Contributor Author

apblack commented Nov 15, 2018

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
Copy link
Contributor

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 apblack changed the title Type Syntax forall in Type Syntax Mar 7, 2023
@apblack
Copy link
Contributor Author

apblack commented Mar 7, 2023

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
Copy link
Contributor

KimBruce commented Mar 8, 2023 via email

@apblack
Copy link
Contributor Author

apblack commented Mar 8, 2023

@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
Copy link
Contributor

KimBruce commented Mar 8, 2023 via email

@apblack
Copy link
Contributor Author

apblack commented Mar 9, 2023

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
Copy link
Contributor Author

apblack commented Mar 17, 2023

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
Copy link
Contributor

KimBruce commented Mar 18, 2023 via email

@kjx
Copy link
Contributor

kjx commented Mar 18, 2023

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
Copy link
Contributor

kjx commented Mar 20, 2023

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
Copy link
Contributor

KimBruce commented Mar 21, 2023 via email

@apblack
Copy link
Contributor Author

apblack commented Mar 22, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants