Hacker News new | comments | show | ask | jobs | submit login
Bootstrapping a Type System (2010) (stuffwithstuff.com)
101 points by lemming 65 days ago | hide | past | web | 22 comments | favorite



For those of you don't know, Bob Nystrom is the developer of Wren (wren.io), and previous to it he developed Magpie (the language he's discussing), and Finch (http://finch.stuffwithstuff.com/). He's pretty impressive as far as language development goes.


I don't know about impressive, but I'm definitely profuse. :)


He also wrote the excellent Game Programming Patterns, which you can read here:

http://gameprogrammingpatterns.com/


I've read a few of this guys blog posts and they are generally fairly interesting. This one a little less so, but I had a good chuckle from the line about why he implemented generics in magpie. "Magpie has generics because I’m firmly of the opinion that a type system without generics is about as useful as a language with functions but no parameters." Let the go programmers pour hate upon this blog post


You can obviously write a code generator for all the functions you need once you write an AI good enough: by eliminating extraneous features like generics, Go leaves you free to actually solve problems that matter.

(/s)

Edit: I won't speak about the obvious, but anyone going back in my post history and concluding "Haskell Evangelism Strikeforce with an axe to grind" with a smirk is probably mistaken. There are well-designed languages whose goals may not perfectly align with mine (hello C/Elm/Clojure) and then there are some whose confusing inconsistency of design is, well ... confusing.


Funny enough, I think you've actually hit the nail on hm the head about what makes go programmers so irritating, that they think the go spec has somehow taken into account "the right way" for every possible problem. It's so obnoxious.

Problems that actually matter is such a good indicator that someone has no idea what they're talking about.

Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing


> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing

And that's what makes Haskell evangelists intolerable. (Even if Haskell isn't your favourite language).

Go has it's place.

C has it too, especially on devices with > 32kb memory.

I adore Scheme and it's spec, it's expressiveness, and flexibility. Doesn't mean I think it's the best language for running a game engine, though it has been done.

We all have reasons we like our languages, and what they can be, and what they're good for.

But no language is the be-all, and end-all, of languages. There are always trade-offs. It just can't be helped.

Awk is amazing at dealing with small bits of information, quickly. It's a full language, that has been used to write some large programs... But it isn't as well suited to that. As a scripting language however, it's great.

Python is my go-to for prototyping. It can be a tad inconsistent, and more verbose than my tastes, and weaker typing than I'd like, but it works well enough.

Can't we all just get along?


C is glorious. After a bunch of years screwing around with a bunch of different languages, I believe popularity is an indicator of local optima. C hit so many important points, it became critical. I think it blew its competition away, 40 years ago.

Go people have a point. Haskell people have a point. Their points aren't as strong as c's was, back in the day, so they don't dominate in the way c did.

We don't have a clear winner right now. Different languages bring different things. We are in another exploration phase of languages.


C has so many decisions that feel odd, but make so much sense! (Yes, I love C).

I'm in the process of building a tiny programming language for some Arduinos, as part of a homebrew computer.

I'm making the memory space as a stack.

But how to have a variable know it's location in the stack?

Return an int! Oh, I just reinvented the typeless pointer C has.

PLT exploration is fun, exciting, and love reading about experiments like Magpie and Wren.

But... I still use C99 at work every day, and there's nothing wrong with that.


> C has it too, especially on devices with > 32kb memory.

Can I assume you mean, devices with < 32kb memory? Or is there another language you would use on devices with such as small amount of memory instead of C?


The local assembler? Fortran? Forth?

Personally I would prefer C. But I can see arguments for each of the above.


Sorry, less than.

100 > 32.


> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing.

You're guessing either way. By formalizing and using deductive proof on those forms, you're guessing that your forms correctly model the intended behavior, which gets harder as the forms get more powerful and abstract. You can 100% guarantee the properties that follow from the forms. You can't deductively prove that your forms are the right forms, and that becomes more important--and harder to verify--as the forms get more abstract and powerful.

Which is what irritates me about static typing zealots. Static typing is useful in that it provides deductive guarantees, but it's not free and does have tradeoffs and pitfalls. Instead of requiring 100% guarantees of correctness, you can relax it and require sufficient guarantees of correctness, which will enable you to use the same mechanisms to inductively prove more useful things more easily, and allow you to use the same mechanisms to verify more assumptions and properties than is reasonably possible with formal verification. That's a tradeoff that should be considered more often than it is.

A primitive example of this is the use of unit tests to replace some of the formal proofs done by type checkers. There are undervalued advantages to writing programs that way--leaning on inductive instead of deductive guarantees of correctness.


The point of a type system is 100% guarantees. Honestly, if it fails at that, I'm not sure it becomes useful at all for correctness (it may still be useful for operation overloading).

Now, of course, nearly all systems have many properties that you don't want to enforce by the type system. Proofs are hard work, better do them only where it's easiest or really important.

Yet, most times I hear the phrase "static typing zealots", it comes from somebody that does not have experience with a good type system and is thus completely unable to weight off the work of constructing your types and the one of getting enough tests to be sure your program works.


> Problems that actually matter is such a good indicator that someone has no idea what they're talking about.

> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing

This is how you become irrelevant. "Problems that actually matter" are the problems that actually matter - matter to the people who are trying to write programs. If you're trying to write proofs, then formalizing and proofing matter. More of us are trying to write programs, though.


I think "proof" shouldn't be taken too literally. At the end stronger type system make easier to craft correctly working programs and less lottery machines.


I think it is other way around. It is non-Go programmers who would pour hate on lack of generics in Go every time. It is irrespective of whether Go is even referred in blog post or not.


Well when his language generates revenue we can discuss usefulness in objective terms, until then it lacks any real bite.


what is the relation between "language generates revenue" and "usefulness in objective terms"?

is the latter necessarily dependent on the former?


Revenue is an objective measure of usefulness because cash can be traded for any service, it's not the only one, but it is definitely one of the most important.


it seems to me that revenue is so distant from programming language that you possibly aren't measuring what you think you're measuring.


I followed this blog for a long time. The whole journey of creating the Magpie language is fantastic. Most of what I know as a senior dev comes from trying to really understand his posts.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: