Posted: May 15, 2012 10:41 pm
by VazScep
SpeedOfSound wrote:I am completely torn between two poles on strong typing. As long as you can over-ride everything the I am a fan.
You have no constraints when you're in front of a Turing machine.

"It's not about what the language makes possible; it's about what it makes easy."

When it comes to brass tacks, the difference is that typed languages make it easy to write typed programs and make it difficult to write untyped programs.

I would like to dig into some of these new languages but not sure if I have the time. Tell me a about a pretty thing or two. I've got my head inside medium densely spiny neurons right now so I will probably disappoint you.
Take implication in logic. I gave two axioms governing the logic of implication earlier on in the thread. Here's the first:

p → q → p

Now in Haskell, if you ask for the type of the constant function, you get this:

Code: Select all
> :t const
const :: a -> b -> a

As I suggested in the OP, there's more here than a mere analogy. Implications are the type of functions. If I tell you that p implies q, I'm telling you that I can meet the specification that inputs a p and outputs a q.

From there, the strength of the analogy goes crazy.