Hi all, I want to learn something from you, because this is an argument I know rather superficially.
Here the question: from the viewpoint of a functional-languange (FP) programmer, what concept from lambda calculus (LC) (untyped, typed, ...) are very useful?
Just a comment to better explain my answer: If the theme was Category Theory (CT) for FP, I would respond: mono/epi morphisms, functors, monads, ... (the classics!)
For LC, I would be able to be less precise and less sure.
Well, LC can help gain better intuition about types. If you follow LC from simply typed all the way to dependently typed languages (and beyond!), you can gain a better understanding of these things.
Additionally, you can also see how to do proofs at the type level, how they are related to logics, and how popular provers are related to FP (like Agda or Idris, even Coq to some extent).
Hi all, I want to learn something from you, because this is an argument I know rather superficially.
Here the question: from the viewpoint of a functional-languange (FP) programmer, what concept from lambda calculus (LC) (untyped, typed, ...) are very useful?
Just a comment to better explain my answer: If the theme was Category Theory (CT) for FP, I would respond: mono/epi morphisms, functors, monads, ... (the classics!)
For LC, I would be able to be less precise and less sure.
Well, LC can help gain better intuition about types. If you follow LC from simply typed all the way to dependently typed languages (and beyond!), you can gain a better understanding of these things.
Additionally, you can also see how to do proofs at the type level, how they are related to logics, and how popular provers are related to FP (like Agda or Idris, even Coq to some extent).
I think you can also learn these things from CT, but it it's a rather advanced topic there, as opposed to pretty much basic level of Type Theory.
Vladimir Ciobanu said:
Yes, indeed...