It sounds like you're drawn in the direction of type theory. Lucky for you,
there's a new "Little" book out that sounds perfect for you, "The Little Typer"
by Friedman and Christiansen. It won't help with the jargon at all, but it
covers the subject really well, and after reading it you should be able to
easily figure out the jargon. And it does so in Pie, a language hosted on
Racket.
After The Little Typer, you'll probably still be hungry. I'd recommend
following it with the Coq'Art. It's free in French, and available as a physical
book in English. (If you can speak French, also check out the recordings of the
lectures that Xavier Leroy is giving at the Collège de France. His "from System
F to the Calculus of Constructions" lesson was amazingly clear and
understandable)
On December 1, 2018 10:37:32 AM GMT+01:00, Chansey wrote:
>Dear all,
>
>This question has little to do with Racket, please forgive me if it's
>not
>suitable for posting here.
>
>After reading Paul Graham's book "Hackers & Painters", I became
>fascinated
>with Lisp, so I chose Racket for learning Lisp.
>Now, I have finished reading the trilogy of the scheme: HtDP, SICP, and
>
>EoPL (100% SICP exercise finished, 90% EoPL exercise finished).
>
>Then, what's the next?
>
>In fact, before learning Lisp, I have been using some programming
>languages, such as C, Java, Javascript, Erlang, Haskell, etc.
>I also have some knowledge of computer foundation, such as computer
>architecture, os, computation theory, compiler, network, database, web
>etc...
>Learning Lisp taught me a lot of important concepts in programming
>languages, such as generative recursion, y-combinator, stream, cps,
>type-check/infer, etc...
>
>But in some programming forums (eg: Lisp/Haskell forums), there are a
>lot
>of jargons, which still confuse me, especially about type systems, such
>as:
>What is Existential type?
>What is Dependent type?
>What is Refinement type? (Note: I found typed-racket support this
>experimental features)
>What is Intersection type? (Note: typed-racket support union type, but
>what's intersection type?)
>What is Rank-N type?
>What is System F?
>What is Type reconstruction?
>What is Algebraic data type (ADT)? (What's the difference between sum
>type
>and union type? Why the type "B -> A" is exponential type？What is the
>relationship between ADT and cartesian closed category? What is
>cartesian
>closed category?)
>What is Abstract interpretation?
>What is Partial Evaluation? (not partial application)
>What is Curry–Howard correspondence? (such as "propositions as types")
>What is Lambda cube?
>...
>
>As you can see, most of these jargons involve type systems.
>
>Yes, EoPL does have some basic knowledge of type systems.
>I even implemented the AlgorithmW of Hindley–Milner in Racket, but I
>still
>don't understand these jargons above...
>
>Someone told me that if you want to learn type system, you have to
>learn
>Haskell.
>In fact, I have read Graham Hutton's "Programming in Haskell".
>I can write Haskell, I can write parser combinator, I understand
>functor/applicative/monad/,... But I still can't understand the
>sentence:
>"A monad is just a monoid in the category of endofunctors, what's the
>problem?"
>What? What is endofunctors? what is category,...
>That means I don't really understand monad...
>
>Other people said: if you really want to understand type systems, you
>have
>to understand Lambda cube?
>OK, what is Lambda cube and how to learn it?
>
>Of course, in addition to the type system, there are many other
>programming
>concepts that I did not understand, such as communicating sequential
>processes (CSP), actor model, π-calculus, denotational semantics,
>etc...
>
>I am deeply aware that I lack systematic programming language
>knowledge.
>So can you recommend some books about these advanced topics?
>I've searched some books on Amazon:
>Types and Programming Languages
>Type Theory and Formal Proof
>Concepts, Techniques, and Models of Computer Programming
>
>Since I am self-taught now, I don't know which book I should read
>first, or
>there is other better one to recommended?
>Come back to the main topic: What's the next book, after HtDP SICP and
>EoPL?
>
>Thanks in advance.
>
>Regards,
>Chansey
>
>--
>You received this message because you are subscribed to the Google
>Groups "Racket Users" group.
>To unsubscribe from this group and stop receiving emails from it, send
>an email to racket-users+unsubscr...@googlegroups.com.
>For more options, visit https://groups.google.com/d/optout.
--
Sent from my Android device with K-9 Mail. Please excuse my brevity.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
