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

81–90 of 103 posts

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

#81

Post by danblick »

People sometimes ask on HN about good books on implementing programming languages.

One of the best textbooks I know on type theory is also a pretty good book for getting a programming language up and running: Types and Programming Languages by Ben Pierce.

https://mitpress.mit.edu/books/types-and-programming-languag...

The book starts off implementing the untyped lambda calculus and then adds more and more interesting kinds of types. There's a tarball somewhere on the course website that has all the code from the book, and it's kind of fun to play with all the systems it covers.

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

#82

Post by dmitriid »

dahauns wrote: post #80
dmitriid wrote: post #77

Earlier quoted context omitted.

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

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.

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

#83

Post by psygnisfive »

danblick wrote: post #81

People sometimes ask on HN about good books on implementing programming languages. One of the best textbooks I know on type theory is also a pretty good book for getting a programming language up and running: Types and Programming Languages by Ben Pierce. https://mitpress.mit.edu/books/types-and-programming-languag... The book starts off implementing the untyped lambda calculus and then adds more and more interesting…

I'd also recommend Practical Foundations for Programming Languages (PFPL). And a bunch of other things, which I outlined here:

So You Want To Learn Type Theory (http://purelytheoretical.com/sywtltt.html)

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

#85

Post by tom_mellior »

psygnisfive wrote: post #79
junke wrote: post #73

Earlier quoted context omitted.

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 `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->_G1213),
    Tab = ((a->b)->a->b),
    Tc = [_G1251]^ ((c->_G1251)->c->_G1251),
    Tcd = ((c->d)->c->d) .
Note how both Tab and Tcd arise from instantiating the same schema Typ, which is unchanged.

To avoid binding variables in the schema, you just make sure to only instantiate instances (copies) of the schema:

    abstract_type(Term, Typ) :-
        type(Term, [], T),      % type/3 defined by parent
        term_variables(T, Vars),
        Typ = Vars^T.

    apply_type(Typ, Arg, Result) :-
        copy_term(Typ, TypCopy),  
        TypCopy = Vars^T,
        Vars = [Arg | RemainingVars],
        (   RemainingVars = []
        ->  Result = T
        ;   Result = RemainingVars^T ).

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

#86

Post by gizmo385 »

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.

I don't think that's a particularly good way to judge the problem though. Sure, the JavaScript example might be shorter, but which implementation is safer? Which is going to be easier to work with in the future? I'd make the assertion that the JavaScript version will have a lot more edge cases that could have been caught sooner with a more robust type system.

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

#87

Post by junke »

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

Thanks!

Just to expand on my previous example, I can simply modify how bindings are looked up and generalize the associated type when it is not unknown:

    type(V,Env,T) :-
        ground(V),
        member(V:P,Env),
        generalize(P,T).

    generalize(P,T) :- nonvar(P), !, copy_term(P,T).
    generalize(T,T).
Let's add two rules for tuples and addition, and change the syntax of let for clarity:

    type((A,B),Env,TA * TB) :-
        type(A,Env,TA),
        type(B,Env,TB).

    type(A+B,Env,number) :-
        type(A,Env,number),
        type(B,Env,number).

    type(let(X == XE, E),Env,ET) :-
        type(XE,Env,XT),
        type(E,[X:XT|Env],ET).
Then, typing this:

    let(identity == lambda(v,v),
        let(increment == lambda(x,x+1),
            let(compose ==
                lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))),
                (apply(apply(compose,identity),identity),
                 apply(apply(compose,increment),increment)))))
... gives:

    (_1775 -> _1775) * (number -> number)
You could also make use of meta attributes, ie. data stored inside variables, to control what happens during unification.

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

#88

Post by junke »

psygnisfive wrote: post #79
junke wrote: post #73

Earlier quoted context omitted.

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

Yes, details are tricky. Thanks for the detailed comment.

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

#89

Post by sctb »

Dylan16807 wrote: post #67
sctb wrote: post #66

Earlier quoted context omitted.

Snarky one-liners aren't good comments for Hacker News. You can always say something substantive instead, and then we have a much higher chance of an insightful discussion. https://news.ycombinator.com/newsguidelines.html

It's snarky but I think the replies constitute a perfectly good discussion and there's no reason to collapse all of it by default. It's a bit off-topic but out of the five current top-level comments only one is addressing the contents of the article anyway...

OK, that's a good point. We've uncollapsed the thread.

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

#90

Post by fasquoika »

Cyph0n wrote: post #33
alkonaut wrote: post #15

Earlier quoted context omitted.

My point exactly. If people who liked type systems could stand to use the JS type system (and I only barely managed to write type system without scare quotes), we wouldn't have TypeScript. Or Cofeescript. Or Purescript. Or Elm. Or Fable. Or Flow. Or even ES6.

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?
Post reply on HN