Summer of Programming Languages

Post by coldtea » Mon, Jul 07, 2014, 12:36 PM UTC

fit2rule wrote: post #20

aidenn0 wrote: post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

I would say its because academic researchers don't spend nearly enough time actually using these languages industriously in the worst-case scenarios. If more effort was spent in understanding how, for example, SIL-4 (safety integrity level 4) development is done with non-type-safe languages (hint: code coverage tests, tests, tests..), then there would (imho) be less motivation to continually churn out 'new solutions…

Post by lmm » Mon, Jul 07, 2014, 1:00 PM UTC

coldtea wrote: post #32

lmm wrote: post #10

Earlier quoted context omitted.

Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value. (For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wr…

> Academics don't care so much about things like programming speed. I don't know. Haskell and OccamL, for one, are much, much faster than Python and Ruby.

Post by freyrs3 » Mon, Jul 07, 2014, 1:23 PM UTC

seanmcdirmid wrote: post #29

chriswarbo wrote: post #27

Earlier quoted context omitted.

"Statically-typed" and "type-safe" don't mean the same thing. "Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-chec…

Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?

Post by [deleted] » Mon, Jul 07, 2014, 1:43 PM UTC

freyrs3 wrote: post #35

seanmcdirmid wrote: post #29

Earlier quoted context omitted.

Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?

> DL people are like...what's the difference The dynamic typing folks don't care to provide a definition of types and overload the term to mean many things, the static typing folks have a rigorous one.

Post by seanmcdirmid » Mon, Jul 07, 2014, 1:50 PM UTC

freyrs3 wrote: post #35

seanmcdirmid wrote: post #29

Earlier quoted context omitted.

Well, to people like Bob Harper, there is no such thing as a dynamic "type" (they are tags instead). The argument over terminology appears on comp.types every once in awhile. Then there are people into dynamic languages who swear they have more than one type and actually check these types at run type. Then the static type theorists say...you are just checking tags, and the DL people are like...what's the difference?

> DL people are like...what's the difference The dynamic typing folks don't care to provide a definition of types and overload the term to mean many things, the static typing folks have a rigorous one.