Representing types

[vrandezo]

I talked with @cyrus- and he recommended a few books and papers that might help with getting the eneyj system right, so I started reading "Types and Programming Languages" by @bcpierce00

Good thing, reading the first 100 pages, everything it was talking about was implemented. Yay!

But then it came to typing functions, and it seems that just typing them as Z8 Function is insufficient (which did bite me a few times already). So what we need is to type them in a generic way, including the return type and the argument types.

And then, if we need generic types anyway, well, we can also use them for Z10 List etc.

So, how to do generic types? Here's the suggestion.

Turn all generic types (which includes Z2 Pair, Z10 List, and Z8 Function) into functions that return a Z4. And then the type is something like Function(Boolean, [Boolean, Boolean]) for And.

But now if the signature includes the type, what about the argument declaration? They are still useful for giving the arguments names. But they are not really necessary anymore?

Any thoughts?

[thadguidry]

Something like Type Erasure in Java? https://www.baeldung.com/java-generics#type-erasure This JEP218 might also provide some food for thought in the greater context of parametric polymorphism.

[arthurpsmith]

So what would be the 'type' of Z8 then? Function(Type, [Type, List])? I don't quite see how this works, but it sounds intriguing... How would you express that in json?

In general I think we need to think a bit more about inheritance here. There is already something implicit here with Z1 - zobject as a type; I don't think you have any entity so far that is explicitly of type Z1, but Z1 encompasses all types, so that an object that takes a Z1 argument is actually able to accept any type. So maybe explicitly typed functions (with return type and arguments) can coexist here with a general Z8 - rather than change the meaning of Z8 as it is, perhaps new zobjects should be created for the generics?

[vrandezo]

@thadguidry kinda. The advantage we have is that we have no polymorphism, so it can be hopefully easier.

[vrandezo]

@arthurpsmith yes, that's a great point. I was hoping that the type of the add function would indeed be something like Function(Boolean, [Boolean, Boolean])

In JSON notation, we first would need a Quote mechanism, say, Z99 is the same as Z7 but it is quoted (as in Lisp). So Add would look like:

{
  "Z1K1": "Z8",
  "Z1K2": "Z57",

But it could look like this instead:

{
  "Z1K1": {
    "Z1K1: "Z99",
    "Z99K1": "Z8",
    "Z8K1": "Z50",
    "Z8K2": [ "Z50", "Z50" ]
  },
  "Z1K2": "Z57",

Now if you unquote the Z99, you'll get

  "Z1K1: "Z7",
  "Z7K1": "Z8",
  "Z8K1": "Z50",
  "Z8K2": [ "Z50", "Z50" ]

which is the function call Z8(Z50, [Z50, Z50]), and when that is evaluated we get a new object of type Z4.

But we can use the quoted function for checking that is a function and its argument types easily.

Now as you point out, Z1 is a form of any type already. So should there be something like an any-function type, and probably yes, because what else would be the the signature of a function such as Z592 signature? (Hmm, could it be Z8(Z1, Z1), though?)

So unsure about the latter thing.

Thoughts are welcome.

[arthurpsmith]

The quoting approach might be reasonable. Presumably it could be nested? So you could have

  {
  "Z1K1": {
    "Z1K1": "Z99",
    "Z99K1": "Z8",
    "Z8K1": {
      "Z1K1": "Z99",
      "Z99K1": "Z8",
      "Z8K1": "Z50",
      "Z8K2": ["Z50"]
    }
    "Z8K2": [ "Z50", "Z50" ]
  },...

if you wanted the function to return a function rather than a number or whatever Z50 is?

Without something like that we would get a combinatorial explosion of types...

[vrandezo]

Yes, absolutely!