3 ms·
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 qu
by 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 agoIf 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. ):