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.

Reply via email to