Proof of concept rtype type checker.

[Raynos]

I've added rtype support to my type checker on a branch.

https://github.com/Raynos/jsig2/tree/rtype#rtype-compatibility-branch

I've documented what is implemented, not implemented and what is missing from rtype.

So far I the main piece missing is a way to declare the types of variables or functions. TypeScript and flow have declaration syntax for this.

The other thing I observed is all of the predicate stuff with interfaces is pretty much unimplemented. As it stands interfaces in rtype have "too many features"

I've also ported an example to what I believe is idiomatic rtype ( https://github.com/Raynos/jsig2/blob/rtype/examples/2-memory-db.hjs )

[Mouvedia]

Good job!

You can find the builtins that the MVP will have here.

Is %Boolean%%Mixed related to #73?
Would you be interested in #62 or #42?

[Raynos]

@Mouvedia Correct; Boolean%%Mixed internal type is related to Boolean(Any). I use it for now until I implement mixed as a full type.

It is a type that is effectively a Boolean when used; however you can assign any type into it. It's different from Any because:

var foo: %Boolean%%Mixed = 2;
!foo; // legal
if (foo) {} // legal

foo.bar; // illegal, type Boolean does not have field bar.

[Raynos]

@Mouvedia

As for #42 I've long wanted to improve the existing parser for the type definition language. The main reason for improving is improved error messages, the current ones are quite confusing.

I'm not sure if a BNF based parser will give improved error messages, the current error messages do show line & column offset.

As for #62 The original version of jsig (before jsig2 rewrite ) had runtime checking and wrapping. This was getting really complicated and provided less value then a static type checker. For these reasons I punted on it.

What I do want to do is make sure that I can write a JSON parser helper that makes reading JSON statically type safe. this might be based on validators or based on a typed json parser itself. Statically type safe validation will solve most of my "dynamic type checking" needs.

[Mouvedia]

So you can't do var foo: %Boolean%%Mixed = new Boolean(2);?
If you see any reason to reopen #73 plz comment there.

From your "Not implemented" list Id prioritize:

• Limited builtin type support, we do not support arbitrary javascript value expressions, only strings and numbers.
• Any. One of the core principles of my type checker is correctness. Any place where Any is used we should use mixed instead. The type checker implements flow based restrictions and reflection to be able to operate on mixed.

You shouldn't work on generics just yet: it's still being discussed.

What's in progress?
What's next?

[Raynos]

@Mouvedia

https://github.com/Raynos/jsig2#progress--020-

This tracks current progress; the features I want to work on are mentioned there, including generics.

I'll need a good reason to implement Any. I think I have baseline level Builtin support but need to add:

• Symbol. Not really sure what that is yet, only have ES5 covered
• Date. Havn't written any code related to Date yet.
• Map, Promise, Proxy, Set, WeakMap, WeakSet, other features not implemented as I'm targetting ES5 at the moment
• Predicate, not implemented, don't really know how to yet.

[Mouvedia]

We need at least the "primary builtin types"* + Any and Void.

* https://github.com/ericelliott/rtype/pull/42/files#r59980276

[ericelliott]

Predicate should be relatively easy. It's just a convenient name for the type (...args: Any[]) => Boolean.

Predicate literals are MUCH harder. They pull the entire JS specification into scope. Is there a way to punt on predicate literals and still do mostly OK type checking?

[Raynos]

@ericelliott I think predicate literals are not needed for static type checker to work.

Here's a 2016 paper on adding "refinement types" to TypeScript ( http://arxiv.org/pdf/1604.02480.pdf ). I think implementing predicate / refinement / dependent types is still a research level topic.

[ericelliott]

@Raynos I agree. I'm willing to remove Predicate literals from the spec entirely, if it makes tooling easier. Do you think we should?

[ericelliott]

implementing predicate / refinement / dependent types is still a research level topic.

I think regular expressions fall into that category, but regular expressions can add significant richness to the capabilities of the runtime type checker without adding any complexity at runtime.

Come to think of it, so can predicate literals. Hmm...

Back to the question: Can static type checkers work around them? Is there any way we can add fallback types? For instance, all regular expressions can fall back to Strings, which causes a reduction in type fidelity, but should still work.

Not sure how fallbacks would work for predicate literals... ideas? Am I talking crazy?

[ericelliott]

We might be able to leverage another library (e.g. codemix/contractual) to cover our limitations.

The limitations are on the static analysis side. On the runtime side, literals just work by the magic of a fully functional javascript engine.

[Raynos]

@ericelliott regex string types are better handled as String or "a" | "b" | "c"; those are the two types of strings you can deal with in a typesystem.

Anything else where you want a regex over a string please pass in a structured tuple or object.

interface UserInstance {
  name: /\w+/,
  description?: '',
  likes?: [],
  data?: {}
}

This interface really means name: String. Your trying to put runtime validation and type checking into the same set of concerns.

The difference between runtime validation, is generally that it's done in a single place, where you get user input. Where as type checking is done every single place a type is used, at every variable assignment, at every function call, at every mutation.

[ericelliott]

@Raynos I see your point, and yes, that's how it usually works.

However, at runtime, predicate function (and by extension, regex) type checks work just fine at function call time, and I don't see a really good reason not to include those features in rtype + rfx.

I also don't see a big difference between a structural type that checks:

interface Foo: {
  'a': String,
  'b': Number
}

...and a regex that checks that a string value has one or more letters. name: /\w+/ is basically shorthand for a very large union type.

These things work as expected at runtime... the difficulty static type systems have is that static type systems seek a formal mathematical proof, and if the entire scope of a language as complex as JavaScript (or even RegEx) comes into play, you introduce the possibility of an impossible proof.

Runtime checking doesn't have the restriction of trying to prove that type errors are impossible in any permutation of the running program state. All they care about is "does the current value satisfy the conditions of this predicate right now?"

Static type systems necessarily sacrifice some expressiveness to accomplish the goal of a thorough type correctness proof.

[Raynos]

@ericelliott

The problem with implementing a regex /\w+/ is that we have to track flow typing.

// createUser(name: String) => UserInstance
function createUser(name) {
  return { name: name, ... }
}

This function is a type error; the only way it would be correct is if we did something like

// createUser(name: String) => UserInstance | null
function createUser(name) {
  if (/\w+/.test(name)) {
    return { name: name, ... }
  }

  return null;
}

Forcing developers to do these types of checks can get frustrating; also if a developer uses an "equivelant" but not literally the same regex the static type checker will get confused as well.

You can achieve this with runtime checking, it will work. However the reason I'm working on a static checker is because I do not want the runtime boilerplate and I do not want the runtime overhead.

[tomek-he-him]

@Raynos, literals are needed not only for validation, but also for documentation. Documentation is one of the main goals of rtype.

I like @ericelliott’s idea about fallbacks for static type checking. A regex literal falls back to String, a function literal falls back to whatever is explicitly stated afterwards:

interface Integer
  (number) => number === parseInt(number, 10);
  { ...Number }

We may even enforce stating the fallback via spec.

In that case it’s no overhead on the static analysis side. It’s only a little more overhead on the parsing side – but this syntax is there already and would need to be covered by the parser anyway.

[ericelliott]

@Raynos Again, I see your point that trying to implement /\w+/ is problematic, but I'm not suggesting that a static type checker should do that. I'm suggesting that we use fallback types in the static type checker.

I understand that this introduces the possibility of allowing a small subset of potential type errors at runtime, but correct me if I'm wrong...

The alternative is that we allow rtype to become less expressive and less useful for both documentation and runtime checking.

I'm willing to listen if there's a compelling reason that fallback types are extremely problematic for static analysis, but I think the compromise would be that we relegate regex and predicates to runtime-only solutions like rfx, which would basically put the type fallback burden on the developer, rather than the type checker.

In other words, if a developer can't do /w+/, they'll manually write String, instead, and the effect becomes essentially the same as the automated fallback. Am I right?

The only difference I can see is that now, the type checker can say for certain, "this program conforms to the types as specified", ignoring the fact that the types are now underspecified.

All that said, I feel like I'm missing the major point of your comment.

In your example:

// createUser(name: String) => UserInstance
function createUser(name) {
  return { name: name, ... }
}

Regardless of regex... how is this a type error if we know that UserInstance.name is expecting a string?

At runtime, both the input parameter and the returned object will pass their respective automatically generated predicate functions -- there's no need to write a guard inside the function itself. That's the whole point of automated runtime checking...

Do you mean that you can't infer the type correctness at static analysis time? If so, why not? As far as I can see, as long as UserInstance is specified, you have all the information you need for inference. Am I wrong? If so, please educate me. =)

You can achieve this with runtime checking, it will work. However the reason I'm working on a static checker is because I do not want the runtime boilerplate and I do not want the runtime overhead.

1. You can turn runtime overhead on and off.
2. rtype allows you to forget about in-code guards. They're created automatically for you based on the type annotations.

In other words, based on this:

createUser(name: String) => UserInstance

interface UserInstance {
  name: String
}

You can create two predicate functions: One that checks the arguments for createUser, and one that checks the UserInstance return value. Tools like rfx conditionally return a wrapped function that runs those checks. If type checking is turned off, rfx will pass through the original function, unwrapped, which means there is no call time overhead.

Note that runtime checkers can be completely stripped at compile time for production, so it won't even impact the payload if that's what you want.

[Mouvedia]

@Raynos there have been some changes on our side. Nothing major but I just wanted to keep you posted.

cf #96 https://github.com/ericelliott/rtype#tuples

[ericelliott]

@Raynos Hey, it's been a while. I have a proposal for higher-kinded type support in Rtype. I'd love it if you could take a look and weigh in on whether we could implement it in a type checker like jsig.

[Raynos]

@ericelliott

I've given up on the jsig project. It turns out that TypeScript can implement features faster then I can.

I would recommend using TypeScript; using their type language and system and opening issues around correct-ness.

[ericelliott]

@Raynos Thanks for the status update. It's possible that TypeScript could become a viable alternative in the future, but right now it lacks some critical features:

1. Higher-kinded types (which is what I'm currently trying to make happen for rtype) -- this has been proposed for TypeScript, but there is already a lot of momentum into a type system that would hinder adaptation to higher-kinded types
2. 100% co-expressive compatibility with standard JavaScript (TypeScript doesn't have this without higher-kinded types)
3. Runtime reflection (they're working on this)