From (2014) people!
It was also front page on HN at the beginning of 2015 ;)
So you want to write a type checker (2014)
71–80 of 103 posts
Re: So you want to write a type checker (2014)
#72Perhaps I don't want to just type-check, but I want to do type-inference as well.
Ahh, well! That's a trickier problem! You need a bidirectional system that has unification for metavariables, and then some system for handling unsolved metavars. But to do that requires a more complicated set up. The goal of the post was to introduce the core ideas and show that it's relatively simple to do decent chunks of this stuff. :)
Re: So you want to write a type checker (2014)
#73Perhaps I don't want to just type-check, but I want to do type-inference as well.
Ahh, well! That's a trickier problem! You need a bidirectional system that has unification for metavariables, and then some system for handling unsolved metavars. But to do that requires a more complicated set up. The goal of the post was to introduce the core ideas and show that it's relatively simple to do decent chunks of this stuff. :)
Type inference can be easy too, here is a 5mn Prolog thing:
type(X,_,number) :- number(X).
type(V,Env,T) :-
ground(V),
member(V:T,Env).
type( ET) :-
type(E,[X:XT|Env],ET).
type(apply(F,E),Env,T) :-
type(E,Env,ET),
type(F,Env,ET->T).
type(let(X,XE,E),Env,ET) :-
type(XE,Env,XT),
type(E,[X:XT|Env],ET).
?- type(lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))),[],T).
T = ((_232 -> _226) -> (_225 -> _232) -> _225 -> _226)Re: So you want to write a type checker (2014)
#74Earlier quoted context omitted.
Covariant: A variable needs to have an Animal. You can put a Cat in the variable. Contravariant: A variable needs to have a function that accepts Animals. You can't put a function that accepts only Cats, or it will crash on other kinds of animal. But you can put a function that accepts all LivingThings. So when something is covariant you can use a more specific type, and when it's contravariant you can use a more gen…
Which use cases are those?? Are any of them actually real life, practical use cases?
If a function takes an array of Animal as an argument, the "intuitive" assumption is that you can pass in a Cat[] to it since it's probably processing the array items and a Cat is an Animal.
In usual Javascript patterns, this intuition works, but it's not sound, since arrays are mutable; the function could write to the array, appending a Dog or a Potoo or a Jellyfish- valid for an Animal[] argument, but not sound for a Cat[].
In practice, in most JS code I've seen, arrays are constructed once and then are passed around as immutable collections, so Typescript's unsoundness saves a lot more casting than it introduces errors.
Re: So you want to write a type checker (2014)
#75Earlier quoted context omitted.
The reasons why people accuse JavaScript of being a terrible hack just never really resonated with me. The "wat" video is funny, but that stuff just isn't a problem in my experience. Sure, I've been confused by "array.map(parseInt)" and other oddities, but overall, I think weird semantic edge cases are mostly an easy thing to nitpick about. So as I see it, JavaScript is a nice little language with good syntax for lit…
I don't think js it's a hack. Yes, in the beginning there were some strange things, like objects based on prototype, referring to this, and probably more. Much of this has been worked on, and fixed (unfortunately-but-understandably keeping the old behaviors as well). But nowdays there are many who want more-- they want types --and not only simple types, but some advanced type system. This is where it's hard to see th…
The overlap between people who love Haskell and people who love Nix is huge, yet Nix has no static typing!
Sure, people recognize that a good static type system could improve Nix, but they also recognize that making such a thing isn't easy and that advanced type systems steepen language learning curves.
I just try to counter the meme that people have to take a side and can't simultaneously appreciate very different languages. :)
Re: So you want to write a type checker (2014)
#76Earlier quoted context omitted.
Hi. I'm interested in type theory, and I'm a big fan of JS. shrug Is it really so hard to believe? Imagine if the browser's scripting language didn't have closures or prototypical inheritance. It was possible. JS was a pretty good compromise between power and simplicity.
> Hi. I'm interested in type theory, and I'm a big fan of JS. fan of JS as a whole package (Language, ecosystem, ...) or JS only as a language? The whole package is very attractive, and I can see how people accept ES5 (the language) for the opportunity to work with JS the ecosystem. JS the language I think has some cool features and with ES6 it's even an acceptable language to work with, but I just fail to come to te…
Imagine a program to implement JS vs Java. Which would be shorter?
That's why it seems fair to say that JS is much simpler than Java.
Re: So you want to write a type checker (2014)
#77Earlier quoted context omitted.
TS doesn’t have exhaustiveness checking
I know TS discriminated unions may not be the most elegant construct in the world, but in what way is the check via the never type (as a return or assertion parameter after the switch) not an exhaustiveness check?
“exhaustiveness checking”: automatically making sure that we’ve covered all of the possible cases anywhere that we interact with a piece of data [1]
Typescript doesn’t do that.
There’s a way to manually force exhaustive checking with discriminating unions: https://github.com/basarat/typescript-book/blob/master/docs/...
However, it’s a manual workaround.
[1] Quoted from http://www.adamsolove.com/js/flow/type/2016/04/15/flow-exhau...
Re: So you want to write a type checker (2014)
#78Earlier quoted context omitted.
These languages exist because: - people want to target browsers - everyone’s idea of a perfect language is different - javascript is the only viable compilation/transpilation target Even if Javascript had the combined typing capabilities of Haskell, Agda, and Coq, there would still be people inventing/porting other languages to support client-side web development
There would exist some languages that compile to javascript. But look at typescript specifically. Its compilation stage is mostly "remove the type annotations, so the browser doesn't get confused". The lack of typing is so bad that notable languages get made just to tackle that single issue.
There would exist multiple languages which compile to Javascript.
There’s a reason JS, and Java, and Python, and Rust, and ... and ... and ... exist even though Haskell exists
Re: So you want to write a type checker (2014)
#79Earlier quoted context omitted.
Ahh, well! That's a trickier problem! You need a bidirectional system that has unification for metavariables, and then some system for handling unsolved metavars. But to do that requires a more complicated set up. The goal of the post was to introduce the core ideas and show that it's relatively simple to do decent chunks of this stuff. :)
Type inference can be easy too, here is a 5mn Prolog thing: type(X,_,number) :- number(X). type(V,Env,T) :- ground(V), member(V:T,Env). type( ET) :- type(E,[X:XT|Env],ET). type(apply(F,E),Env,T) :- type(E,Env,ET), type(F,Env,ET->T). type(let(X,XE,E),Env,ET) :- type(XE,Env,XT), type(E,[X:XT|Env],ET). For example: ?- type(lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))),[],T). T = ((_232 -> _226) -> (_225 -> _232) ->…
Indeed! Tho this is only half the problem, because `T` there includes metavariables, so it's not a type but rather a schema at the meta-level for types. What we'd like is something like `forall a b c. (b -> c) -> (a -> b) -> a -> c` so that composition can be used at arbitrary choices of the types. So like, while we can use this composition function at any particular place we need composition, we can't define `compose` to have this type because the first use site will force the metavars to have a particular value and then we get a nasty global monomorphism. We need to explicitly have metavariables in the language itself, rather than at the metalevel of doing the synthesis/checking.
Re: So you want to write a type checker (2014)
#80Earlier quoted context omitted.
I know TS discriminated unions may not be the most elegant construct in the world, but in what way is the check via the never type (as a return or assertion parameter after the switch) not an exhaustiveness check?
“exhaustiveness checking”: automatically making sure that we’ve covered all of the possible cases anywhere that we interact with a piece of data [1] Typescript doesn’t do that. There’s a way to manually force exhaustive checking with discriminating unions: https://github.com/basarat/typescript-book/blob/master/docs/... However, it’s a manual workaround. [1] Quoted from http://www.adamsolove.com/js/flow/type/2016/04/1…
Hm? Typescript actually uses the same mechanism for exhaustiveness checking as flow (like your link describes).