WIP: JSig spec

[Raynos]

I started working on a more formal spec.

I've defined the following statements

• assignment
• type declaration
• import statements

I've defined the following Types

• builtin types
• custom type literals

cc @Matt-Esch @jden

cc @bryan-m-hughes Hi, we talked at forwardjs about typed javascript! I started working on a spec for this kind of stuff, would love some feedback :)

[Raynos]

@jden would love some feedback on this one ;)

The spec is really hard to structure and format correctly.

[junosuarez]

Ah, k. I merged as a WIP and to get more visibility when browsing on GH from the root of the repo.

[junosuarez]

Overall thought on style of the spec: it is still very narrative and example-driven, similar to the readme. It seems like a more formal spec should have an outline something like

1. intro / what / why
2. primitive types
3. syntax
   • labels
   • functions
   • rest parameters
4. combinators
5. import / inline comment / symbol semantics
6. grammar

I don't think that type inference has to be included in the actual spec, since it seems like it would be tool-specific, but I could be convinced otherwise.

[nebrius]

Sorry, I just now saw this (I've been at Outside Lands for the past three days), there's some good stuff here.

I'd like to echo what @jden has to say about creating a more formal structure.

Also, I noticed that you mentioned "null is not of type Object". While the nature of null is confusing and slightly broken in JS with considering null to sometimes be an object, I do wonder how this deviation will affect, say, casting null as an Object, e.g.

type Foo : { bar: String }
foo : Foo

when combined with

var foo = null;

I do disagree with @jden though in that I think that type inference should be included in the spec, somewhere. Perhaps not in spec.md, but I do think it's important to describe how types are inferred. Type inference isn't always 100% obvious, and sometimes you simply have to make an arbitrary decision between two options on how to infer. Type inference can also be aggressive or conservative in terms of look-ahead, inference depth, etc (how do you handle overloading, how do you do generics, how many levels of inference do you do before giving up if you do support generics, etc).

Since you have the "Any" type, this implies that jsig is an optional type system. Going back to type inference, have you thought about how you are going to handle mixing typed and untyped values? E.g. what happens when you pass an "any" type into a function with typed arguments?

[Raynos]

@bryan-m-hughes I need to do a better formal thing in terms of structure.

As for the null thing, I'm not really thinking of using type definitions for variables, i.e. I will probably only specify types for functions or module.exports statements.

In those cases specifying x : Object | null is not too tedious because it's quite rare.

I was thinking of just inferring magically all local variables.

I'm definitely thinking of this being an optional type system mostly for public interfaces of modules.

I was imagining I would get all kinds of wonderful and horrible inferred types of local things. I'm not really sure how I'm going to build a full type checker :/

[junosuarez]

This is the most ready example I could find of doing this sort of type inference in js https://github.com/puffnfresh/roy/blob/master/src/typeinference.js

[nebrius]

Ugh, long single files are something of a pet peeve of mine (I know I know personal preference and all that).

It's incomplete, but CommaScript also does type inference (https://gitlab.theoreticalideations.com/nebrius/commascript/tree/master). As I mentioned at ForwardJS, I'm doing a refactor on it, so the more modern implementation in the type_refactor branch is very incomplete, but the type system is more fleshed out in it. You can get the gist in any case.

The basic idea is to use an AST parser like Esprima or Uglify to walk the source code's AST. You write code that inspects each node and, if it's an expression, returns an inferred type. These inferred types get passed back the call stack and mutated until you reach a statement (statements don't have a type, at least not in any meaningful way).

The master branch of CommaScript doesn't do generics, which I tend to view as essential for an inferred type system, which is why I'm rewriting is, so be warned I guess.

[Raynos]

@bryan-m-hughes Do you think there might be an oppurtunity to have overlap in the actual type inference & type system between commascript & jsig.

Obvouisly the syntax, tooling and approaches are different, but maybe we can re-use some code because we are both walking an esprima AST tree and inferring the types of the nodes in a JS AST tree.

[nebrius]

@Raynos I've been thinking about actually, and tl;dr I'm skeptical, but at the same time it's worth spending more time thinking about.

Here are a few areas I have identified within the type systems where CommaScript and JSig differ, at least according to my understanding (please correct if wrong):

null is considered an object/function/array of a specific type in CommaScript (i.e. it's type is Foo for var foo = ('cast(Foo)', null);), but is treated as its own type in JSig.

CommaScript does not support void (by design), except as a return value for a function. It seems like JSig supports void as a first class type though (I think?)

JSig does not support generics, but they are pretty central in CommaScript, i.e. in CommaScript:

function foo(a, b) {
  return a + b;
}
foo(1, 2); // Casts foo as (int, int) => int
foo('hello ', 10); // Casts foo as (string, int) => string

CommaScript does not support the "Any" type (it is strictly typed, through and through), but JSig does.

So the big question is: with these differences, is it still possible to create a common base that provides a meaningfully useful abstraction that also isn't crazy forked? I.e. I would like something more than a few dozen lines, but at the same time not so crazy as, say, WebKit1 was with supporting V8 and JavaScriptCore with conditionals everywhere.

[Raynos]

@bryan-m-hughes

null is considered an object/function/array of a specific type in CommaScript (i.e. it's type is Foo for var foo = ('cast(Foo)', null);), but is treated as its own type in JSig.

I need to think more about this. I would just infer foo : Foo | null

CommaScript does not support void (by design), except as a return value for a function. It seems like JSig supports void as a first class type though (I think?)

void is only supposed to be used for the return type of a function. For simplicity I treat it as a builtin type rather then a special case in the function type.

JSig does not support generics, but they are pretty central in CommaScript, i.e. in CommaScript:

JSig supports generics the spec is just wildly incomplete. See https://github.com/Raynos/jsig/blob/master/test/parser/integration/definitions/jsig.mli and https://github.com/jden/jsig#generic-types

CommaScript does not support the "Any" type (it is strictly typed, through and through), but JSig does.

Any exists to support the notion that Object <: Any and String <: Any.

The only use case of Any that I can find is ( https://github.com/Raynos/jsig/blob/master/test/parser/integration/definitions/min-document.mli#L22 ) where I'm using it as a shorthand for Object | Boolean | String | Number

with these differences, is it still possible to create a common base that provides a meaningfully useful abstraction that also isn't crazy forked?

I didn't communicate how severely incomplete this. Let me do another bunch of pushes to flesh out the spec way more, I'll cc you on the next PR that contains more stuff and contains a section for EVERYTHING even if it's a bunch of TODOs.