"Types Considered Harmful" by Benjamin Pierce

Great link. Does every type theorist have such a playful sense of humor?

I'm not sure this constitutes a Scalar opinion, but there's obviously
a connection between types as contracts enforced at compiletime and
assertions as contracts enforced at runtime. The trick in language
design is to be able to specify contracts that specify what's
important, and no more, and to do it in a way that doesn't result in
too much overhead, particularly at runtime. Scala's type system seems
to have hit a pretty sweet spot in this regard, but I wonder whether
it's the last word.

A

On Fri, Sep 16, 2011 at 9:56 AM, Alex Cruise wrote:
> Obviously the author of TAPL doesn't think types are harmful in general, but
> there are some interesting issues at play.  I'd love to hear some Scalar
> opinions on this:
> http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf
> -0xe1a

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 09/17/2011 12:18 PM, Archontophoenix Quar wrote:
> Great link. Does every type theorist have such a playful sense of humor?
>
> I'm not sure this constitutes a Scalar opinion, but there's obviously
> a connection between types as contracts enforced at compiletime and
> assertions as contracts enforced at runtime. The trick in language
> design is to be able to specify contracts that specify what's
> important, and no more, and to do it in a way that doesn't result in
> too much overhead, particularly at runtime. Scala's type system seems
> to have hit a pretty sweet spot in this regard, but I wonder whether
> it's the last word.
>
> A
>
> On Fri, Sep 16, 2011 at 9:56 AM, Alex Cruise wrote:
>> Obviously the author of TAPL doesn't think types are harmful in general, but
>> there are some interesting issues at play. I'd love to hear some Scalar
>> opinions on this:
>> http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf
>> -0xe1a

Scala is distinct from many others in that its type system is
turing-complete.

On 9/16/2011 9:18 PM, Archontophoenix Quar wrote:
> Great link. Does every type theorist have such a playful sense of humor?
>
> I'm not sure this constitutes a Scalar opinion, but there's obviously
> a connection between types as contracts enforced at compiletime and
> assertions as contracts enforced at runtime. The trick in language
> design is to be able to specify contracts that specify what's
> important, and no more, and to do it in a way that doesn't result in
> too much overhead, particularly at runtime. Scala's type system seems
> to have hit a pretty sweet spot in this regard, but I wonder whether
> it's the last word.
>
> A
>
> On Fri, Sep 16, 2011 at 9:56 AM, Alex Cruise wrote:
>> Obviously the author of TAPL doesn't think types are harmful in general, but
>> there are some interesting issues at play. I'd love to hear some Scalar
>> opinions on this:
>> http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf
>> -0xe1a
>

Arch,

I've heard the opinion on the #channel that there should -never- be an
unexpected type, therefore introspection/reflection are unnecessary.

However, that does not take into account this goldfish bowl in which we
all swim, called, for want of a better name, "reality."

Scala needs to be able to be able to grok the types of things that are
not expected at compile-time. That's necessary for it to be at once an
ethereal experimental academic language, and also an industrial, greasy,
useful one.

Bob (ishmal)

I particularly like slide 66 on page 33, and recommend it to
interested readers as worth pondering. While it states the obvious, it
does it very nicely. To paraphrase it the way I think about it:

Methods to verify software correctness come in 3 complementary
flavours or layers. We should learn and use all 3:

1. Types: General but weak theorems (usually checked statically). [eg
Scala type system]
2. Laws: General and strong theorems, checked dynamically for
particular instances [eg Scalacheck, Design by Contract, Assertions]
3. Examples: Specific and strong theorems, checked quasi-statically
on particular “interesting instances” [eg Unit tests, BDD specs,
Manual testing]

My perception is that Laws are under-appreciated in the Scala world,
while Type Systems are still under-appreciated in the wider industry.

-Ben

On Sat, Sep 17, 2011 at 2:56 AM, Alex Cruise wrote:
> Obviously the author of TAPL doesn't think types are harmful in general, but
> there are some interesting issues at play.  I'd love to hear some Scalar
> opinions on this:
> http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf
> -0xe1a

I suspect Type-systems are under appreciated because certain popular languages,*cough* Java *cough*, make strong, static types very painful and to some extent I think dynamiclanguages like Python and Ruby have benefited from that pain to woo users interested in results rather than compiler wrangling.
As a current Python developer Scala is wooing me because it seems to makestrong, static Types pleasant again :-)

On 18 September 2011 16:29, Ben Hutchison <brhutchison@gmail.com> wrote:

I particularly like slide 66 on page 33, and recommend it to
interested readers as worth pondering. While it states the obvious, it
does it very nicely. To paraphrase it the way I think about it:

Methods to verify software correctness come in 3 complementary
flavours or layers. We should learn and use all 3:

1. Types:  General but weak theorems (usually checked statically). [eg
Scala type system]
2. Laws:  General and strong theorems, checked dynamically for
particular instances [eg Scalacheck, Design by Contract, Assertions]
3. Examples:  Specific and strong theorems, checked quasi-statically
on particular “interesting instances” [eg Unit tests, BDD specs,
Manual testing]

My perception is that Laws are under-appreciated in the Scala world,
while Type Systems are still under-appreciated in the wider industry.

-Ben

On Sat, Sep 17, 2011 at 2:56 AM, Alex Cruise <alex@cluonflux.com> wrote:
> Obviously the author of TAPL doesn't think types are harmful in general, but
> there are some interesting issues at play.  I'd love to hear some Scalar
> opinions on this:
> http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf
> -0xe1a

On Mon, Sep 19, 2011 at 11:00 AM, Adam Jorgensen <adam.jorgensen.za@gmail.com> wrote:

As a current Python developer Scala is wooing me because it seems to makestrong, static Types pleasant again :-)

Just so.  I was very enamored of Ruby back in the early 2000s, because it allowed me to do type stuff that Java just couldn't hack.  (And allowed far less painful functional programming.)  But Scala gives me basically all that *and* nice compiler-time type checking, so it won me back to the static side of the force...