[Caml-list] Hitchhiker's Guide to Typing

[Caml-list] Hitchhiker's Guide to Typing

[Hao-yang Wang]

>A Hitchhiker's Guide to type theory (and all the other alien things my eyes
>glaze over at on this list) aimed at the unwashed masses would go a long
>way to making OCaml (and functional programming in general) more
>accessible.  Did I pass over one somewhere?

I think by "type theory" you mean the type systems used in modern 
programming languages. Luca Cardelli has written some nice 
tutorial/survey on this topic.

See <http://www.luca.demon.co.uk/Bibliography.html>. Look for the 
articles "Typeful programming" and "Type systems".

Cheers,
Hao-yang Wang
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Hitchhiker's Guide to Typing

[leary]

On Fri, Jun 08, 2001 at 01:22:05PM -0700, Hao-yang Wang wrote:
> I think by "type theory" you mean the type systems used in modern 
> programming languages. Luca Cardelli has written some nice 
> tutorial/survey on this topic.
> 
> See <http://www.luca.demon.co.uk/Bibliography.html>. Look for the 
> articles "Typeful programming" and "Type systems".

Excellent resources (particularly the "Typeful" doc).  My thanks to you. :)

Seems to beg the questions tho': Is it not possible to learn and use OCaml
without wading through 60 page docs on typing?  Will I have to read more of
these papers to learn the object system?  Modules?

I'm willing to read up on typing, since it seems pretty important to
getting a good handle on FPLs/OCaml, and that's definitely what I'm after,
but I wonder (in advance) if 60 pages can't be turned into far fewer.  I'd
like some feedback on the notion that "if you can't explain it to a
five-year-old, you don't really understand it" (or, rather, haven't given
the simplest, most concise, most practically useful explanation).  By way
of a couple examples, the HHGTTG entry for Earth is "mostly harmless".
Investing can be distilled down to "buy low, sell high".  Not crashing a
motorcycle is a matter of "look where you want to go, don't look at the
ground".  No discussion of gyroscopic effects and psychology.  Of course,
a working knowledge of typing will never be so simple, but contrast, for
example, the "Type Systems" doc above; Table 34 is a good place to look.
This is not what 99.99% of people looking to understand typing in OCaml are
going to want.  If I didn't have a burning desire to learn OCaml/ML, and
someone gave me just this document (and thanks for including the other
one!) as a way of explaining the typing lingo, I'd give up and go back to
what I was doing before, assuming that OCaml was every bit as obscure,
difficult, and unrewarding as Unlambda:

http://www.eleves.ens.fr:8080/home/madore/programs/unlambda/


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

[Caml-list] Re: Hitchhiker's Guide to Typing

[Joseph R. Kiniry]

I have my students/friends read Cardelli's "Typeful Programming", mentioned 
below, before teaching/introducing any language with typing.  It is the 
most readable summary of the topic that I know.

My HHGTTG entry for OCaml (or other languages with similarly strong type 
systems) would be "bad things don't unexpectedly happen when your run the 
program".  That seems to be good enough to interest the friends that I 
continue to convert.

Best,
Joe
--
Joseph R. Kiniry                    http://www.cs.caltech.edu/~kiniry/
California Institute of Technology        ID 78860581      ICQ 4344804


--On Friday, June 08, 2001 04:32:11 PM -0700 leary@nwlink.com wrote:

> On Fri, Jun 08, 2001 at 01:22:05PM -0700, Hao-yang Wang wrote:
>> I think by "type theory" you mean the type systems used in modern
>> programming languages. Luca Cardelli has written some nice
>> tutorial/survey on this topic.
>>
>> See <http://www.luca.demon.co.uk/Bibliography.html>. Look for the
>> articles "Typeful programming" and "Type systems".
>
> Excellent resources (particularly the "Typeful" doc).  My thanks to you.
> :)
>
> Seems to beg the questions tho': Is it not possible to learn and use OCaml
> without wading through 60 page docs on typing?  Will I have to read more
> of these papers to learn the object system?  Modules?
>
> I'm willing to read up on typing, since it seems pretty important to
> getting a good handle on FPLs/OCaml, and that's definitely what I'm after,
> but I wonder (in advance) if 60 pages can't be turned into far fewer.  I'd
> like some feedback on the notion that "if you can't explain it to a
> five-year-old, you don't really understand it" (or, rather, haven't given
> the simplest, most concise, most practically useful explanation).  By way
> of a couple examples, the HHGTTG entry for Earth is "mostly harmless".
> Investing can be distilled down to "buy low, sell high".  Not crashing a
> motorcycle is a matter of "look where you want to go, don't look at the
> ground".  No discussion of gyroscopic effects and psychology.  Of course,
> a working knowledge of typing will never be so simple, but contrast, for
> example, the "Type Systems" doc above; Table 34 is a good place to look.
> This is not what 99.99% of people looking to understand typing in OCaml
> are going to want.  If I didn't have a burning desire to learn OCaml/ML,
> and someone gave me just this document (and thanks for including the other
> one!) as a way of explaining the typing lingo, I'd give up and go back to
> what I was doing before, assuming that OCaml was every bit as obscure,
> difficult, and unrewarding as Unlambda:
>
> http://www.eleves.ens.fr:8080/home/madore/programs/unlambda/
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Hitchhiker's Guide to Typing

[Brian Rogoff]

On Fri, 8 Jun 2001 leary@nwlink.com wrote:
> On Fri, Jun 08, 2001 at 01:22:05PM -0700, Hao-yang Wang wrote:
> > I think by "type theory" you mean the type systems used in modern 
> > programming languages. Luca Cardelli has written some nice 
> > tutorial/survey on this topic.
> > 
> > See <http://www.luca.demon.co.uk/Bibliography.html>. Look for the 
> > articles "Typeful programming" and "Type systems".

If, like me, you like to see a working implementation, then download a 
copy of "Basic Polymorphic Typechecking" from this page. Also, Michael 
Schwartzbach wrote a nice little tutorial called "Polymorphic Type
Inference" which you can get here 

http://www.brics.aau.dk/BRICS/LS/95/3/BRICS-LS-95-3/BRICS-LS-95-3.html

There are little parts of this that I think could be better, but overall 
I like it best. If you work through it you'll learn a lot. 

> Seems to beg the questions tho': Is it not possible to learn and use OCaml
> without wading through 60 page docs on typing? 

Sure. But you'll understand these things a lot better if you apply
yourself and read some of these papers. I agree that many of the papers 
go too deep too fast. 

> Will I have to read more of these papers to learn the object
> system?  Modules?

No, but once again you'll learn a lot from the papers. For objects and
modules 

http://caml.inria.fr/~remy/cours/appsem/
http://caml.inria.fr/~xleroy/publi/modular-modules-jfp.ps.gz

> I'm willing to read up on typing, since it seems pretty important to
> getting a good handle on FPLs/OCaml, and that's definitely what I'm after,
> but I wonder (in advance) if 60 pages can't be turned into far fewer.  I'd
> like some feedback on the notion that "if you can't explain it to a
> five-year-old, you don't really understand it"

That notion is nonsense. I understand differential calculus quite well,
and I doubt I could explain it to a five year old. In fact, as a TA for  
an introductory numerical analysis class at Snodfart (name changed to
protect the guilty :) I gave a simple explanation of Taylor's Theorem to a 
masters student in CS who just couldn't get it. Not a very good student,
no doubt, but probably better equipped than a five year old. 

> (or, rather, haven't given the simplest, most concise, most practically
> useful explanation).  By way of a couple examples, the HHGTTG entry for
> Earth is "mostly harmless". Investing can be distilled down to "buy
> low, sell high".  Not crashing a motorcycle is a matter of "look where
> you want to go, don't look at the ground".

None of these are useful. My explanation for everything can be distilled
to "Shit happens", but that's also not very useful.

> Of course, a working knowledge of typing will never be so simple, but
> contrast, for example, the "Type Systems" doc above; Table 34 is a good
> place to look.

I've got a copy of Stroustrup's "The C++ Programming Language" here. That's 
not simple. Nor is Wall's Perl book, nor the Common Lisp Hyperspec, nor
the Ada 95 LRM. 

If you want a working knowledge of OCaml, write lots of code. Use the
papers to flesh out that working knowledge to a deeper understanding. 

-- Brian


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Hitchhiker's Guide to Typing

[Jonathan Coupe]

> > I'd
> > like some feedback on the notion that "if you can't explain it to a
> > five-year-old, you don't really understand it"

My feedback: whoever first said this was probably a professional politician
or a journalist.

Jonathan  Coupe


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

[Caml-list] Re: Hitchhiker's Guide to Typing

[Joseph R. Kiniry]

--On Monday, June 11, 2001 07:22:12 PM +0100 Jonathan Coupe 
<jonathan@meanwhile.freeserve.co.uk> wrote:

>> > I'd
>> > like some feedback on the notion that "if you can't explain it to a
>> > five-year-old, you don't really understand it"
>
> My feedback: whoever first said this was probably a professional
> politician or a journalist.
>
> Jonathan Coupe

Note that the proper quote from which, I believe, this semi-derives is:

The Nobel Laureate Richard Feynman was once asked by a Caltech colleague to 
explain why spin 1/2 particles obey Fermi Dirac statistics. He responded, 
"I'll prepare a freshman lecture on it." But a few days later he returned 
and said, "You know, I couldn't do it. I couldn't reduce it to the freshman 
level. That means we really don't understand it."

This is quoted in _Six Easy Pieces_, _Six Not So Easy Pieces_, and, I 
believe, _Surely You're Joking Mr. Feynman_.  A web search via Google with 
"Feynman" and "lecture" will reveal more.

Joe
--
Joseph R. Kiniry                    http://www.cs.caltech.edu/~kiniry/
California Institute of Technology        ID 78860581      ICQ 4344804
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Hitchhiker's Guide to Typing

[David Fox]

"Jonathan Coupe" <jonathan@meanwhile.freeserve.co.uk> writes:

> > > I'd
> > > like some feedback on the notion that "if you can't explain it to a
> > > five-year-old, you don't really understand it"
> 
> My feedback: whoever first said this was probably a professional politician
> or a journalist.

In any case, certainly not a parent.
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr