"Please don't complain about tangential annoyances—e.g. article or website formats, name collisions, or back-button breakage. They're too common to be interesting."
may be worth mentioning in this case that firefox reader mode (the little cartoon icon of a printed page in the address bar) is helpful. also firefox will remember an increased font size setting for oleg's site if you hit ctrl-+ a few times
It incrementally covers normalization by evaluation, bidirectional typechecking, basic pattern unification, implicit insertion (which relies on unification), and then more sophisticated variants on pattern unification.
I'm more familiar with F#, so I got stuck at this line:
type ('a,'b) app += List_name : 'a list -> ('a,list_name) app
I understand that app is an extensible type and this line adds a union case called List_name to the type, but the signature of List_name confuses me. If I write (List_name x) is x a list or a function?
The variable "x" would be a list in this case. This the GADT (Generalized Abstract Data Types) syntax, where the type of the whole union can depend on the discriminated union case. Thus
List_name: 'a list -> ('a, list_name) app
reads: for any value "x" of type "'a list", "List_name x" constructs a value of type "('a, list_name) app". In this case, it is the the "list_name" tag part of the type which is dependent on the union case.
12 comments
[ 5.2 ms ] story [ 51.3 ms ] threadhttps://news.ycombinator.com/newsguidelines.html
I wonder how much this is a problem in practice, aside from the type-checker taking too long.
It incrementally covers normalization by evaluation, bidirectional typechecking, basic pattern unification, implicit insertion (which relies on unification), and then more sophisticated variants on pattern unification.