Friday, October 5, 2012

Type systems

It rankles, because I'm thoroughly a liberal-language kind of guy, but ... type systems [wiki] have their place, and a programming semantics that makes any claim to being comprehensive certainly can't avoid them.  What brought them back to my attention is a blog post by one of the creators of Rust.  The problem with the blog post is, I can't understand it.  I have thought so very little about type semantics over the years that it's as though the author were speaking a different language.

So: task.  Think about type semantics and how they might profitably be incorporated into Decl.  Clearly types will have to be a part of the declaration of a value, and equally clearly they'll have to be part of a functional part of the system (functional in the sense of functional language, a modality I also want to support due to its strongly declarative nature).

One more feature.  It really is going to be a kitchen-sink language.  I should probably just break down and go find a reasonably detailed syllabus of computer science and just put everything in there.  (I'm not actually kidding.  It's all "semantics of programming".)

On that note, see also Microsoft's new open-source typed Javascript language that compiles to Javascript: TypeScript.  This might honestly be a good place for me to start.

Essentially, I see type systems as providing assertions about the usage of certain constructs in the program.  At compile time (note: Decl has no compilation step, so "at checking time" - checking being a specific action in that case), the compiler checks everything you've told it and makes sure it's all consistent.  That's essentially all type checking is.  You can get very, very ramified with the semantics of your typing system, and it looks like that might be what the Rust blog post is about (the syntax is writing checks the semantics can't yet cash) - but the notion of offline examination of some subset of the logic of a program is a valuable one, and one that Decl could very easily embrace.

Especially since I'd like to see a more interactive dialog going on with the editor at some point - type checking should probably be going on all the time, as that's likely to be one more indicator of what you're thinking as you're coding.  So the editor could effectively be coming up with a list of questions you could think of, some of which would include, "Is that what you really meant?  Because you said 'x' was an integer up here."

No comments:

Post a Comment