What's a type?

[apblack]

In one of our test suites, I found this code:

def full = singleton "full"

type OptionNumber =  Number | empty | full

def items = list [6, 7, empty, 9, full]

def block1 = { x:OptionNumber ->
    match(x)
      case {n:Number -> "Number {n}"}
      case {y:empty -> "Singleton {y}"}
      case {z:full -> "Singleton {z}"}
      else {"should not happen"}
}

Is this legal? full is a Pattern, but not a type, as far as I can see; (empty is defined analogously). So is OptionNumber a type? I don't see how it can be.

This used to work in miningrace because Number | empty uses the | operation on a type, which produces another type — although attempting to enumerate the methods in that type would fail with a NoSuchMethod error. I've fixed this (as part of moving the "magic" out of the prelude), and now Number | empty redirects to empty | Number, which used the | operation on the pattern empty to produce a new pattern.

With this new implementation, OptionNumber is a pattern, but not a type, and the type declaration is incorrect. (Making it

def OptionNumber =  Number | empty | full

is fine.)

So, the quesiton is: what does Grace allow? Is the original test legal Grace?

[kjx]

So, the quesiton is: what does Grace allow? Is the original test legal Grace?

The short answer is: what’s the return type of “singleton”

If it’s something like “singleton(value:Object is manifest) -> Type[staticTypOof(value)]” then what’s the problem?

Au courage, mon braves: the semantics are clear even without the “is manifest”

J

[apblack]

The return type of singleton(name:String) is something like

EqualityObject & Pattern

In fact, here are the definitions, from the new standard dialect that I'm in the process of creating for minigrace

trait singleton {
    use BasePattern
    use identityEquality
    method matches(other) { self.isMe(other) }
}

trait singleton (nameString) {
    use singleton
    method asString { nameString }
}

If you think that the type and implementation should be something else, please show me. What are the implementation and type in Hopper, Kernan and Moth?

[kjx]

I'm pretty sure they just don't have it. But none of them claim to have a full library.

James

On 23/11/2019, at 19:02PM, Andrew Black notifications@github.com wrote:

If you think that the type and implementation should be something else, please show me. What are the implementation and type in Hopper, Kernan and Moth?

[apblack]

They don’t have what? Types? Singletons? We agreed in issue #100 that singleton generated pattern objects, not types. Are you suggesting that we reopen that?

[kjx]

they don't have "singletons" in their minimal library, nor static type checks in any case. In those designs, the static checker would be the one to enforce that distinction - J

On 26/11/2019, at 15:47PM, Andrew Black notifications@github.com wrote:

They don’t have what? Types? Singletons? We agreed in issue #100 that singleton generated pattern objects, not types. Are you suggesting that we reopen that?

[apblack]

The dynamic type checker must also know what a type is. For example, one can ask dynamically whether one type conforms to another.

I'm deducing from the conversation here that:

1. As discussed in April 2016 in issue #100, no one then knew how to make Singletons types consistent with the meaning of type in Grace (a disjunction of interfaces)

2. Nothing has changed since then.

3. The minigrace test that declared OptionNumber a type predates this design decision, and is now wrong. It was added (by @apblack) as test t168 in commit 3bb25f788d8d, in October 2014. According to the commit message, this was "based on Kim's Number | empty example". This was the same commit that added the Singleton object constructor to the standard prelude.

4. In the motivating test, OptionNumber should instead be declared as a def. With this change, the test passes.

5. If someone has a concrete proposal for types that include types that uniquely-describe singleton objects, they should make it — I suggest as a new design issue, referencing this and #100.

6. I'm closing this issue.