Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

So you want to write a type checker (2014)

languagengine.co

Post reply on HN
Print view View original

91–100 of 103 posts

Re: So you want to write a type checker (2014)

#91

Post by fasquoika »

sillysaurus3 wrote: post #76
alkonaut wrote: post #70

Earlier quoted context omitted.

> 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.

At the very least, the size of the standards of the two are comparable. JS is far too inconsistent to be truly simple

https://www.ecma-international.org/publications/files/ECMA-S...

https://docs.oracle.com/javase/specs/jls/se9/jls9.pdf

Re: So you want to write a type checker (2014)

#92

Post by hinkley »

tangent128 wrote: post #74
tytytytytytytyt wrote: post #58

Earlier quoted context omitted.

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…

The real problem here is that mutable data structures aren’t entirely type sound. The solution here is to split collections into read only and mutable types, but people balk at this.

At one point long ago I did some experiments with this, and found that the most of the unique method signatures necessary to represent the data structures we are familiar with are concentrated in the mutators.

That is, the interface differences between read only data structures are pretty small. So you don’t double the surface area by splitting read from write. It’s more like 25%, and this might be partially offset by simplifications in code that has to scan multiple types of collections.

Re: So you want to write a type checker (2014)

#93

Post by psygnisfive »

tom_mellior wrote: post #85
psygnisfive wrote: post #79

Earlier quoted context omitted.

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 `compos…

Prolog variables are metavariables, if you use them as such. ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ). Typ = [_G947, _G948]^ ((_G947->_G948)->_G947->_G948) . ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ), apply_type(Typ, a, Ta), apply_type(Ta, b, Tab), apply_type(Typ, c, Tc), apply_type(Tc, d, Tcd). Typ = [_G1179, _G1180]^ ((_G1179->_G1180)->_G1179->_G1180), Ta = [_G1213]^ ((a->_G1213)->a->…

mm.. perhaps I'm just not familiar enough with prolog, but I don't think it's possible to extract out a set of Prolog-level metavariables and compute over them? This is what's necesary to turn something like `_G947 -> _G947` into `forall a. a -> a`. but probably I just don't know enough. cool if you can, tho!

Re: So you want to write a type checker (2014)

#94

Post by erikpukinskis »

alkonaut wrote: post #29
lhnz wrote: post #27

Earlier quoted context omitted.

This is probably generally true in terms of the language itself, but one assumes that there are people that love type-theory yet also like JavaScript for its ecosystem, environment-reach and hackability. And perhaps there are people that enjoy the difficulties in trying to type a language which is very dynamic.

Yes the deployment model of js runtimes is second to none. As are the runtimes themselves. The ecosystem is vibrant (though perhaps a bit chaotic) JS the language (ES5 in particular) and its standard library is really all thats laughable about JS.

You say that as if the two were unconnected.

The simplicity of ES5 is exactly why it is everywhere. It tackled the security and distribution model first, and everything else second.

And I’m a little hurt that you think my code is laughable. I write exclusively in ES5. Maybe read my code first and then insult me. But do it in a substantive way. Don’t just laugh at us like an asshole.

I’m not trying to insult your code without having read it.

Re: So you want to write a type checker (2014)

#95

Post by alkonaut »

alkonaut wrote: post #29
lhnz wrote: post #27

Earlier quoted context omitted.

This is probably generally true in terms of the language itself, but one assumes that there are people that love type-theory yet also like JavaScript for its ecosystem, environment-reach and hackability. And perhaps there are people that enjoy the difficulties in trying to type a language which is very dynamic.

Yes the deployment model of js runtimes is second to none. As are the runtimes themselves. The ecosystem is vibrant (though perhaps a bit chaotic) JS the language (ES5 in particular) and its standard library is really all thats laughable about JS.

> You say that as if the two were unconnected.

They are only connected historically. But since it's obviously possible to use JS as a compilation target and only use its deployment model but none of its language quirks, they are unconnected now at least.

> It tackled the security and distribution model first, and everything else second

This is probably true. And it was also as far as I know not really "designed" to be a large scale general purpose language. It was basically invented in a short period of time to perform simple frontend tasks. Things like scoping, function resolution, module system, representation of integers etc were perhaps not the biggest concern at the time. And I'm not saying the design decisions were inherently BAD, they were probably right at the time! I'm saying the tasks we use JS for now would warrant a more thuroughly designed language. And of course ES6 is that, to a large degree - so that's good.

ES5 isn't the only language that ever outgrew it's costume. Every language that reaches enough success so it sticks around will do that eventually. Php, C etc are prime examples of languages that are used in way more places than their creators could have imagined, and as we all know a lot of times C is used because of its portability/deployment model, despite being a very flawed tool for the task.

> And I’m a little hurt that you think my code is laughable. I write exclusively in ES5. Maybe read my code first and then insult me.

I don't think anyones code is laughable, and I haven't seen yours so can't comment on it. I said there are aspects of ES5 the language that make me laugh (and cry). Function resolution, scoping rules, integer representation, equality rules, ...

> Don’t just laugh at us like an asshole. > I’m not trying to insult your code without having read it.

I hope not, but you are free to bash any language I use to write my code all you want and I won't upset about it, and I definitely won't think you are an asshole if you do. I hate tons of aspects of my 9-5 lanugage (C#) and I'd be delighted to discuss it.

Re: So you want to write a type checker (2014)

#96

Post by tom_mellior »

psygnisfive wrote: post #93
tom_mellior wrote: post #85

Earlier quoted context omitted.

Prolog variables are metavariables, if you use them as such. ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ). Typ = [_G947, _G948]^ ((_G947->_G948)->_G947->_G948) . ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ), apply_type(Typ, a, Ta), apply_type(Ta, b, Tab), apply_type(Typ, c, Tc), apply_type(Tc, d, Tcd). Typ = [_G1179, _G1180]^ ((_G1179->_G1180)->_G1179->_G1180), Ta = [_G1213]^ ((a->_G1213)->a->…

mm.. perhaps I'm just not familiar enough with prolog, but I don't think it's possible to extract out a set of Prolog-level metavariables and compute over them? This is what's necesary to turn something like `_G947 -> _G947` into `forall a. a -> a`. but probably I just don't know enough. cool if you can, tho!

That extraction is what the term_variables/2 predicate does that I use in my code. It gives you a list of all unbound variables in the given term. To simulate the quantification, I then just add that list in front of the term with the ^ operator (which has no semantics, it is just the traditional constructor for these things).

So for `_G947 -> _G947` I get the variable list `[_G947]` and use it to represent the universally quantified term as `[_G947]^(_G947 -> _G947)`. If you want to display this with nicer variable names, just substitute names of your choice for the variables in the quantifier list.

Re: So you want to write a type checker (2014)

#97

Post by kreetx »

mbrock wrote: post #75
kreetx wrote: post #59

Earlier quoted context omitted.

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 l…

It's a good discussion!

I think it's more about where are we coming from and where are we going. I have no nix experience (but know bits from reading stuff on the internet :-), but maybe the pro-nix attitude among haskellers is from a few factors: (1) referentially transparent definitions, and (2) it's better than things that have come before. I.e even with other devops/deployment scripting tools nix adds new value, and is in this sense "on it's way somewhere" (perhaps haskellization, but we'll see). So the nix people might move to the typed version when that happens.

But for languages the typed ones are already here, and have been for quite some time. So if one has stuck around with javascript then my question is why (apart from the practicality reasons).

Re: So you want to write a type checker (2014)

#98

Post by dahauns »

dmitriid wrote: post #82
dahauns wrote: post #80

Earlier quoted context omitted.

Hm? Typescript actually uses the same mechanism for exhaustiveness checking as flow (like your link describes).

It does. And, like in the article, Typescript is “saved by a hack”. Compare that to Elm, where it will automatically fail compilation if you don’t include all required types in a switch statement. Without any hacks or manual intervention.

Oh, I know. Elm is far more elegant in that regard.

But just because I have to "switch on" exhaustiveness checks doesn't mean they don't exist.

Re: So you want to write a type checker (2014)

#99

Post by dmitriid »

dahauns wrote: post #98
dmitriid wrote: post #82

Earlier quoted context omitted.

It does. And, like in the article, Typescript is “saved by a hack”. Compare that to Elm, where it will automatically fail compilation if you don’t include all required types in a switch statement. Without any hacks or manual intervention.

Oh, I know. Elm is far more elegant in that regard. But just because I have to "switch on" exhaustiveness checks doesn't mean they don't exist.

Thing is, it only works in if and switch statements, you have to be aware of it (I don’t think you can deduce it from docs), and you have to manually trigger it.

It’s ”poor man’s exhaustiveness” and TS will hopefully get better at this

Re: So you want to write a type checker (2014)

#100

Post by Cyph0n »

fasquoika wrote: post #90
Cyph0n wrote: post #33

Earlier quoted context omitted.

Why is everyone forgetting Scala.js?

Because if they listed every language that compiled to JS the actual point of their comment would get buried?

The focus of the original comment was on compile-to-JS languages with strong(er) type systems. Scala.js should be at the top of that list.

Try again.

Post reply on HN