So you want to write a type checker (2014) • Hacker News Board

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

#101

Post by mbrock » Tue, Oct 31, 2017, 1:37 PM UTC

kreetx wrote: post #97

mbrock wrote: post #75

Earlier quoted context omitted.

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

Yeah, agreed. JavaScript doesn't really have any impressive redeeming features. I like it because it's kind of minimally viable and accidentally really useful for dealing with APIs full of duck typed nested records.

It's really hard to be both minimally viable and have a sound and expressive static type system.

Simply typed lambda calculus isn't even Turing complete, and the fate of Haskell's endless extensions indicates an inherent rabbit hole...

Haskell itself has somewhat horrible issues dealing with extensible records, and the solutions are all complex and hard to understand.

Dealing with JSON in Haskell in a quick and easy way is nowadays quite nice, but it took the invention of van Laarhoven lenses and the aeson-lens module...

I greatly prefer JavaScript to Java because I prefer no static type checking over inexpressive static type checking! And expressive type systems are hard to get right, so it's a very classic "worse is better" situation.

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

#102

Post by tangent128 » Wed, Nov 01, 2017, 2:54 PM UTC

hinkley wrote: post #92

tangent128 wrote: post #74

Earlier quoted context omitted.

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

Do you have any examples lying around of what the interface differences would look like?

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

#103

Post by jonsterling » Sat, Nov 04, 2017, 3:05 AM UTC

hinkley wrote: post #92

tangent128 wrote: post #74

Earlier quoted context omitted.

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

There's nothing wrong with mutable data structures from a type soundness perspective. We know how to do it properly. But you need to get the type system right in order to include mutable data structures; often people get this wrong, and it leads to all sorts of frustration...