▲ | chongli 10 hours ago | |
You don’t need a runtime for dependent types. After type checking the types get erased during compilation. | ||
▲ | whilenot-dev 8 hours ago | parent [-] | |
Nobody would question that, but publishing a JavaScript library means that anyone using plain JavaScript can make use of it. Even though you aren't ever in control of the toolchain of your library's users, it's still your responsibility - as library author - to take that differences into account. If you'd transpile your library from Idris to JavaScript and publish it, these validations just can't be neglected at runtime. Type systems are just another model of the world at runtime. |