5 ms·

Forall.js: Idris-like static types and invariant checks for JavaScript

63 points by LightMachine 9y ago

indolering 9y ago
> the catch is that it isn't doing classical (logical) type-checking, but, instead, it "type-checks" by inspecting with random samples. So it's almost nothing like Idris, which is geared towards formal verification. All of these unsound type systems make development and refactoring easier, but you don't really know what type checks are being done at a lower level. TS* has (had) an untrusted type for input from potentially hostile adversaries. I would have preferred to do high-assurance client side code development in that, but it's no longer maintained.
WaxProlix 9y ago
Not trying to be a downer on the creator, because it's very cool, but I think the best thing that can come from libraries like this is adoption into Typescript. Typing is really better suited to being a part of the language and not a facet of libraries (or is it - an interesting thought there, the ability to import type systems).
- zzzzzzzza 9y ago
  that's (kind've) what facebooks flow tool does (in that you type header at top of the file to turn on type checking)
- gsg 9y ago
  You might be interested in http://blog.racket-lang.org/2017/04/type-tailoring.html http://blog.racket-lang.org/2017/04/type-tailoring.html, which argues for customised type checking.
setra 9y ago
This is really not like the Idris type system at all. Its not even really like the Haskell type system. This is basically doing the same thing as the Haskell quickcheck library but running it at compile time. AKA just testing a function with a few values.
- LightMachine 9y ago
  If it quacks like a type and it types like a type... Just kidding! A type system, in essence, is not much different from that, though - Pi, for example, is basically a type-level lambda that is applied to the typed function (and it is sufficient to express basically any real-world type system). In any case, I hope I made it very clear on the that it is in no means an actual type system, but my dirty way to get invariants and some refined types on plain JS. If we had a mature Idris->JS compiler this hack wouldn't be necessary. ):
phpnode 9y ago
There's a fair bit of work in this area that leverages Flow type syntax, e.g: - https://github.com/gcanti/tcomb https://github.com/gcanti/tcomb - https://github.com/gcanti/io-ts https://github.com/gcanti/io-ts (for typescript) - https://github.com/codemix/flow-runtime https://github.com/codemix/flow-runtime (i wrote this) And another alternative is to use Design by Contract, like Eiffel: https://github.com/codemix/babel-plugin-contracts https://github.com/codemix/babel-plugin-contracts (also me)
- LightMachine 9y ago
  Oh. Thank you very much for linking that. I wish I saw it 3 days ago, though. It is basically the same thing.
chriswarbo 9y ago
I would avoid using the terms "type" and "check" together for this, since "type checking" has a well established meaning (referred to as the "classical"/"logical" approach in this README). Random testing like this, as WaxProlix says, is reminiscent of QuickCheck; in that case you might replace "type" with "property", since the phrase "property checking" is associated with this approach. Alternatively, stick with "type" (or maybe "contract"? These terms are all very overloaded!), but use "testing" instead of "checking". Note that this approach is should be possible in Idris too, since we have equality types. For example, assuming we have some QuickCheck-style functions available, I could say: someProp : Foo -> Bar -> Bool someProp x y = whateverExpressionWeLike somePropCheck : quickCheck someProp = True somePropCheck = refl This will only type-check (in the traditional sense) if `quickCheck someProp` evaluates to `True`; otherwise `somePropCheck` will be ill-typed. `someProp` and `somePropCheck` have no impact at runtime, since they're never called from anywhere (they could be encapsulated privately in a module too). `quickCheck` can be a normal function; it's simple enough to generate "random" values in a pure way (e.g. Mersenne Twister with some arbitrary seed), although that would lose one of the features of property checking: each time it runs, we explore more of the possible inputs, and hence gain more confidence. Since runtime guarantees don't depend on the particular values generated by `quickCheck`, it's still "morally pure" even if implemented in an impure way; hence we could use a mechanism similar to "type providers" to impurely generate random values, and hence regain that feature.
- LightMachine 9y ago
  I agree with everything you said. On doing that in Idris (which is my dream language - the only reason I don't use it is its JS compiler is too slow), would it be possible to randomly generate elements of any data type, or would we have to write an `Arbitrary` instance for every type you want to test? I don't know/remember much about generics on Idris, would love to learn more. (Seriously, though, why is the JS compiler still so slow? Again - I'm willing to put substantial money into funding a better one...)
  - chriswarbo 9y ago
    Hmm, I imagine there's probably a generic way to do it; but I was imagining a straight port of the Haskell version. Note that it might be difficult to generate values of some heavily-constrained dependent type; you'd effectively be implementing a proof search!
jart 9y ago
Closure Compiler already does this. Most JavaScript at Google is written with static types in JSDoc. Closure Compiler also has a DSL (sort of like template metaprogramming) where complicated generic type transitions can be defined with functional expressions. Examples: https://github.com/google/closure-compiler/blob/d1c1673d1d891616144f1f5d0d9642dd1e232612/externs/es6.js#L1110 https://github.com/google/closure-compiler/blob/d1c1673d1d89... and https://github.com/google/closure-compiler/blob/55cf43ee31e80d89d7087af65b5542aa63987874/contrib/externs/angular-1.3-q_templated.js#L98 https://github.com/google/closure-compiler/blob/55cf43ee31e8... Documentation: https://github.com/google/closure-compiler/blob/e7954defc514920469c79349e4742fca4c82fd58/src/com/google/javascript/jscomp/parsing/TypeTransformationParser.java#L53 https://github.com/google/closure-compiler/blob/e7954defc514... and https://github.com/google/closure-compiler/blob/b8d8d1d6c6d245a3df57feedc511f2e849b01932/test/com/google/javascript/jscomp/parsing/JsDocInfoParserTest.java#L3178 https://github.com/google/closure-compiler/blob/b8d8d1d6c6d2... and https://github.com/google/closure-compiler/blob/8829c165b30fdb1937ce7f4285d23ee38ebe3535/test/com/google/javascript/jscomp/TypeTransformationTest.java https://github.com/google/closure-compiler/blob/8829c165b30f... Welcome to what happens when a company hires PhDs to write web pages.
sunesimonsen 9y ago
An alternative that is much easier to adopt, is to use unexpected-check http://unexpected.js.org/unexpected-check/ http://unexpected.js.org/unexpected-check/
be5invis 9y ago
So where is the famous Idris elaborator? Where are the universes? Where’s inductive types? Where are they?
didibus 9y ago
I'm confused. Does this actually statically checks, or is this testing? Like, does it tag everything with type info and walk the code statically without executing it and checks that all connections respect their types? It seems to me it does that for non dependent types, and then it does generative testing for the dependent types? And can also add runtime contracts for them?

63 points by LightMachine 9y ago

> the catch is that it isn't doing classical (logical) type-checking, but, instead, it "type-checks" by inspecting with random samples. So it's almost nothing like Idris, which is geared towards formal verification. All of these unsound type systems make development and refactoring easier, but you don't really know what type checks are being done at a lower level. TS* has (had) an untrusted type for input from potentially hostile adversaries. I would have preferred to do high-assurance client side code development in that, but it's no longer maintained.

WaxProlix 9y ago

Not trying to be a downer on the creator, because it's very cool, but I think the best thing that can come from libraries like this is adoption into Typescript. Typing is really better suited to being a part of the language and not a facet of libraries (or is it - an interesting thought there, the ability to import type systems).

zzzzzzzza 9y ago
that's (kind've) what facebooks flow tool does (in that you type header at top of the file to turn on type checking)
gsg 9y ago
You might be interested in http://blog.racket-lang.org/2017/04/type-tailoring.html http://blog.racket-lang.org/2017/04/type-tailoring.html, which argues for customised type checking.

setra 9y ago

This is really not like the Idris type system at all. Its not even really like the Haskell type system. This is basically doing the same thing as the Haskell quickcheck library but running it at compile time. AKA just testing a function with a few values.

LightMachine 9y ago
If it quacks like a type and it types like a type... Just kidding! A type system, in essence, is not much different from that, though - Pi, for example, is basically a type-level lambda that is applied to the typed function (and it is sufficient to express basically any real-world type system). In any case, I hope I made it very clear on the that it is in no means an actual type system, but my dirty way to get invariants and some refined types on plain JS. If we had a mature Idris->JS compiler this hack wouldn't be necessary. ):

phpnode 9y ago

There's a fair bit of work in this area that leverages Flow type syntax, e.g: - https://github.com/gcanti/tcomb https://github.com/gcanti/tcomb - https://github.com/gcanti/io-ts https://github.com/gcanti/io-ts (for typescript) - https://github.com/codemix/flow-runtime https://github.com/codemix/flow-runtime (i wrote this) And another alternative is to use Design by Contract, like Eiffel: https://github.com/codemix/babel-plugin-contracts https://github.com/codemix/babel-plugin-contracts (also me)

LightMachine 9y ago
Oh. Thank you very much for linking that. I wish I saw it 3 days ago, though. It is basically the same thing.

chriswarbo 9y ago

I would avoid using the terms "type" and "check" together for this, since "type checking" has a well established meaning (referred to as the "classical"/"logical" approach in this README). Random testing like this, as WaxProlix says, is reminiscent of QuickCheck; in that case you might replace "type" with "property", since the phrase "property checking" is associated with this approach. Alternatively, stick with "type" (or maybe "contract"? These terms are all very overloaded!), but use "testing" instead of "checking". Note that this approach is should be possible in Idris too, since we have equality types. For example, assuming we have some QuickCheck-style functions available, I could say: someProp : Foo -> Bar -> Bool someProp x y = whateverExpressionWeLike somePropCheck : quickCheck someProp = True somePropCheck = refl This will only type-check (in the traditional sense) if `quickCheck someProp` evaluates to `True`; otherwise `somePropCheck` will be ill-typed. `someProp` and `somePropCheck` have no impact at runtime, since they're never called from anywhere (they could be encapsulated privately in a module too). `quickCheck` can be a normal function; it's simple enough to generate "random" values in a pure way (e.g. Mersenne Twister with some arbitrary seed), although that would lose one of the features of property checking: each time it runs, we explore more of the possible inputs, and hence gain more confidence. Since runtime guarantees don't depend on the particular values generated by `quickCheck`, it's still "morally pure" even if implemented in an impure way; hence we could use a mechanism similar to "type providers" to impurely generate random values, and hence regain that feature.

LightMachine 9y ago
I agree with everything you said. On doing that in Idris (which is my dream language - the only reason I don't use it is its JS compiler is too slow), would it be possible to randomly generate elements of any data type, or would we have to write an `Arbitrary` instance for every type you want to test? I don't know/remember much about generics on Idris, would love to learn more. (Seriously, though, why is the JS compiler still so slow? Again - I'm willing to put substantial money into funding a better one...)
- chriswarbo 9y ago
  Hmm, I imagine there's probably a generic way to do it; but I was imagining a straight port of the Haskell version. Note that it might be difficult to generate values of some heavily-constrained dependent type; you'd effectively be implementing a proof search!

jart 9y ago

Closure Compiler already does this. Most JavaScript at Google is written with static types in JSDoc. Closure Compiler also has a DSL (sort of like template metaprogramming) where complicated generic type transitions can be defined with functional expressions. Examples: https://github.com/google/closure-compiler/blob/d1c1673d1d891616144f1f5d0d9642dd1e232612/externs/es6.js#L1110 https://github.com/google/closure-compiler/blob/d1c1673d1d89... and https://github.com/google/closure-compiler/blob/55cf43ee31e80d89d7087af65b5542aa63987874/contrib/externs/angular-1.3-q_templated.js#L98 https://github.com/google/closure-compiler/blob/55cf43ee31e8... Documentation: https://github.com/google/closure-compiler/blob/e7954defc514920469c79349e4742fca4c82fd58/src/com/google/javascript/jscomp/parsing/TypeTransformationParser.java#L53 https://github.com/google/closure-compiler/blob/e7954defc514... and https://github.com/google/closure-compiler/blob/b8d8d1d6c6d245a3df57feedc511f2e849b01932/test/com/google/javascript/jscomp/parsing/JsDocInfoParserTest.java#L3178 https://github.com/google/closure-compiler/blob/b8d8d1d6c6d2... and https://github.com/google/closure-compiler/blob/8829c165b30fdb1937ce7f4285d23ee38ebe3535/test/com/google/javascript/jscomp/TypeTransformationTest.java https://github.com/google/closure-compiler/blob/8829c165b30f... Welcome to what happens when a company hires PhDs to write web pages.

sunesimonsen 9y ago

An alternative that is much easier to adopt, is to use unexpected-check http://unexpected.js.org/unexpected-check/ http://unexpected.js.org/unexpected-check/

be5invis 9y ago

So where is the famous Idris elaborator? Where are the universes? Where’s inductive types? Where are they?

didibus 9y ago

I'm confused. Does this actually statically checks, or is this testing? Like, does it tag everything with type info and walk the code statically without executing it and checks that all connections respect their types? It seems to me it does that for non dependent types, and then it does generative testing for the dependent types? And can also add runtime contracts for them?