6 ms·

Type Theory and Functional Programming (1999) [pdf]

197 points by fanf2 1y ago

lugu 1y ago
Is it a good material to dive into this topic today?
- cjfd 1y ago
  Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing rules' in the coq (nowadays rocq) manual. That is a 'slightly' higher friction way of learning this stuff. This document seems to be more pedagogical.
  - avodonosov 1y ago
    Have you found this stuff useful during the many years since you learned it? Or you don't mean you mastered it enough to judge its usefulness?
    - cjfd 1y ago
      I have a personal coq/rocq project regarding the verification of software so for that purpose it is highly useful. I also wrote a proof assistent myself (https://github.com/chrisd1977/system https://github.com/chrisd1977/system).
- quchen 1y ago
  TTOP is the standard work on the topic. Some parts I would say fell out of fashion (using Miranda for example), but many parts are either timeless or still just as relevant. That said, the book is very dense; for me it was just too much the first time I tried to read it. After circling back to it after a while it gets much easier, because you know what parts you really need (which is a common pattern for me at least with everything academic).
  - mogoh 1y ago
    TTOP? Do you mean TTFP?
    - quchen 1y ago
      TAPL, I meant TAPL (Types and Programming languages by Pierce)! This would not have happened with a well-typed comment section. I mixed up OP's book (which is nice as well!) and the abbreviation. Sorry!
      - deleted 1y ago
        [deleted]
  - taolson 1y ago
    Miranda should still be readable for those with some Haskell background (it was a major influence on developing the Haskell language). I also have a more modern update to Miranda called Admiran: https://github.com/taolson/Admiran https://github.com/taolson/Admiran
- ks2048 1y ago
  A related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".
  - 4ad 1y ago
    They are very different books. TAPL is a book about programming language semantics, TTAFP is a programmer-oriented book about Martin-Löf type theory. There is very little overlap. TAPL is definitely the book to pick up if you are interested in programming language semantics. But if you are interested in logic, dependent types, Curry-Howard correspondence there are potentially better and more modern materials than TTAFP (not to say that TTAFP is bad). If you care about formalizing programs Sofware Foundations is a much better resource, and if you care about mathematics and logic, there are resources specifically suited to that.
    - spewffs 1y ago
      What other books would you suggest? I've been reading TTAFP for a few months now and I don't like it very much. I was thinking maybe starting to read Principles of Dependent Type Theory by Angiuli and Gratzer but I'm not sure if it really covers the same area.
  - lo_zamoyski 1y ago
    TAPL is a perfectly good book, but some in academia will tell you that it is somewhat dated.
randomNumber7 1y ago
Why is type theory always tied to functional programming? Wouldn't it be possible to use some of the ideas in imperative languages?
- zelphirkalt 1y ago
  I am guessing, that it is, because imperative processes are very hard to describe properly using type theory. For example: If you have an object, that has some members, that are initially not set, that is a different type than when they are set. So you cannot say that object has exactly one type. After every setting of a member, you have a new type. That's not something that you can statically work with easily. Mutation destroys the type guarantees. The type system can only be on a more limited level, that is rougher and doesn't give as many guarantees, unless you restrict yourself in what you do to your objects. Like for example not mutating them. Or not having nullable members. Things like that. So I think FP is more suitable for type theory research and pondering, and people who are researching in the matter will not even consider doing that for imperative languages, because they have understood long ago, that these languages lack the guarantees, that you can get with FP, and therefore are not worth spending the time on.
  - brabel 1y ago
    That’s just not true. Rust has a wonderful type system and it can encode mutability, which is a must for anything performance oriented. That is a benefit that FP misses out on. You can still analyze Rust programs with a great deal of assurances. The fact that it’s procedural seems to not matter much at all. An example of a language that allows mutability and has a research-level type system is Flix.
    - zelphirkalt 1y ago
      > [...] which is a must for anything performance oriented. But that's also not really true. Using functional data structures it is possible to write highly performant software. Check out for example "CppCon 2017: Juan Pedro Bolivar Puente - Postmodern immutable data structures"[1], an impressive talk, in which someone shows their developed editor that can edit huge text files without lag faster than any mainstream editor today. This is enabled by functional data structures. Usage of functional data structures throughout a project also ensures, that parts can be trivially parallelized, which is not true for traditional algorithms, and therefore can easily scale with number of CPUs available. For more on that subject, you might want to watch a few Joe Armstrong talks. Rust achieves type safety by introducing more language concepts like ownership, borrowing, and lifetimes, to formalize, who has access when and how. It also creates things as immutable by default, unless you make use of `mut`. Unfortunately, Rust's philosophy is shared memory and making shared memory access safe, rather than message passing, which is at odds with FP. [1]: https://www.youtube.com/watch?v=sPhpelUfu8Q https://www.youtube.com/watch?v=sPhpelUfu8Q
denismenace 1y ago
I think in the end step by step functional programming will be widely adopted. Concepts that have a strong theory behind them tend to last longer. Similar to how relational databases and SQL are still the gold standard today.
- deleted 1y ago
  [deleted]
- cubefox 1y ago
  That seems improbable. Pure functional languages are very unpopular according to TIOBE. In particular, interest in Haskell seems to be in decline. Functional features are mostly just an add-on to programming languages with mutable state. By far the most popular language, Python, doesn't even have static typing.
  - bheadmaster 1y ago
    > By far the most popular language, Python, doesn't even have static typing. Arguably, Python is statically typed - it's just that it only has one type: object.
    - wk_end 1y ago
      I know Robert Harper has advanced that argument, but I think it's only really interesting for striking a single rhetorical blow: that, uh, actually statically typed languages are trivially more expressive than Python, since Python has one static type and they have as many as you want. But I think as an actual ontology, as an actual way of understanding and structuring the world, it's obviously quite silly. There's no compile-time (static) type checking phase in Python, because it'd be trivial and therefore a waste of time. Without static type checking, what does it mean to say it's "statically" typed? Moreover, the language has an entirely different, extraordinarily related concept of type which is checked dynamically. Yes, you can say that "Python is a statically typed language with only a single meaningless static type and but also dynamically checked dynamic types", but frankly that's not telling you anything that calling it a dynamically typed language isn't. From a different angle, you can't program SML or something "monotypically" - just restricting yourself to one type - without effectively building an interpreter for an entirely separate, dynamic language inside of it (you can of course build a statically typed language inside of Python, so if you think that counts you're just stripping the meaning from comparing languages). In that sense, Python's just plain doing something fundamentally different from what "a static language with one type" is.
YellowSuB 1y ago
Is this book available in print version anywhere? I am unable to find it except for a used hardcover.
- lo_zamoyski 1y ago
  It's out-of-print.
deleted 1y ago
[deleted]
phoenixhaber 1y ago
[dead]
bedman12345 1y ago
Man I hate functional programming so much. Please, to anyone reading this. Don’t waste your time on this stuff. They always try to claim functional code makes things safer and more elegant, but I have never seen that in reality. These ideas seem to produce terrible code first and foremost.
- jghn 1y ago
  Can you provide objective measures for "terrible code" and then examples of what you're describing?
  - bedman12345 1y ago
    It’s slow. Example: quicksort [] = [] quicksort (p:xs) = (quicksort lesser) ++ [p] ++ (quicksort greater) where lesser = filter (< p) xs greater = filter (>= p) xs It’s really complicated. Everybody includes lenses https://hackage.haskell.org/package/lens https://hackage.haskell.org/package/lens I don’t want to read all that stuff just for imperative syntax. It’d both slow and hard to read. Compare these two: https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/spectralnorm-ghc-4.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/... https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/spectralnorm-gcc-6.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/... The c examples complexity lies in using SIMD. If you know simd it’s easy. You should know simd, it’s useful. The Haskell example is drivel. Long complicated and in the end hopelessly slow compared to the c example. You could als use simd in Haskell, but then it would just be C with extra steps.
    - jrrv 1y ago
      The Haskell looks much better, and I don't even know Haskell. > If you know simd it’s easy. Surely "if you know Haskell it's easy" is equally applicable.
      - bedman12345 1y ago
        > The Haskell looks much better, and I don't even know Haskell Plain crazy take. The c example uses basic coding to implement some clever maths with special fast instructions. Thehaskell example is just some dumb algo implemented with complicated programming. There is obviously nothing good about that. You can also look at a c example without simd https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/spectralnorm-gcc-3.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/... It’s shorter and simpler and faster than the Haskell version. It’s not even close???

197 points by fanf2 1y ago

lugu 1y ago

Is it a good material to dive into this topic today?

cjfd 1y ago
Sure, why not. It seems to be a pretty good exposition of the material. When I got interested in this stuff many years ago I worked my way through the 'typing rules' in the coq (nowadays rocq) manual. That is a 'slightly' higher friction way of learning this stuff. This document seems to be more pedagogical.
- avodonosov 1y ago
  Have you found this stuff useful during the many years since you learned it? Or you don't mean you mastered it enough to judge its usefulness?
  - cjfd 1y ago
    I have a personal coq/rocq project regarding the verification of software so for that purpose it is highly useful. I also wrote a proof assistent myself (https://github.com/chrisd1977/system https://github.com/chrisd1977/system).
quchen 1y ago
TTOP is the standard work on the topic. Some parts I would say fell out of fashion (using Miranda for example), but many parts are either timeless or still just as relevant. That said, the book is very dense; for me it was just too much the first time I tried to read it. After circling back to it after a while it gets much easier, because you know what parts you really need (which is a common pattern for me at least with everything academic).
- mogoh 1y ago
  TTOP? Do you mean TTFP?
  - quchen 1y ago
    TAPL, I meant TAPL (Types and Programming languages by Pierce)! This would not have happened with a well-typed comment section. I mixed up OP's book (which is nice as well!) and the abbreviation. Sorry!
    - deleted 1y ago
      [deleted]
- taolson 1y ago
  Miranda should still be readable for those with some Haskell background (it was a major influence on developing the Haskell language). I also have a more modern update to Miranda called Admiran: https://github.com/taolson/Admiran https://github.com/taolson/Admiran
ks2048 1y ago
A related book (seems to be more often cited) is Types and Programming Languages by Benjamin C. Pierce. That seems to be more concrete (as opposed to theoretical), with chapter titles like "An ML Implementation of {some concept}".
- 4ad 1y ago
  They are very different books. TAPL is a book about programming language semantics, TTAFP is a programmer-oriented book about Martin-Löf type theory. There is very little overlap. TAPL is definitely the book to pick up if you are interested in programming language semantics. But if you are interested in logic, dependent types, Curry-Howard correspondence there are potentially better and more modern materials than TTAFP (not to say that TTAFP is bad). If you care about formalizing programs Sofware Foundations is a much better resource, and if you care about mathematics and logic, there are resources specifically suited to that.
  - spewffs 1y ago
    What other books would you suggest? I've been reading TTAFP for a few months now and I don't like it very much. I was thinking maybe starting to read Principles of Dependent Type Theory by Angiuli and Gratzer but I'm not sure if it really covers the same area.
- lo_zamoyski 1y ago
  TAPL is a perfectly good book, but some in academia will tell you that it is somewhat dated.

randomNumber7 1y ago

Why is type theory always tied to functional programming? Wouldn't it be possible to use some of the ideas in imperative languages?

zelphirkalt 1y ago
I am guessing, that it is, because imperative processes are very hard to describe properly using type theory. For example: If you have an object, that has some members, that are initially not set, that is a different type than when they are set. So you cannot say that object has exactly one type. After every setting of a member, you have a new type. That's not something that you can statically work with easily. Mutation destroys the type guarantees. The type system can only be on a more limited level, that is rougher and doesn't give as many guarantees, unless you restrict yourself in what you do to your objects. Like for example not mutating them. Or not having nullable members. Things like that. So I think FP is more suitable for type theory research and pondering, and people who are researching in the matter will not even consider doing that for imperative languages, because they have understood long ago, that these languages lack the guarantees, that you can get with FP, and therefore are not worth spending the time on.
- brabel 1y ago
  That’s just not true. Rust has a wonderful type system and it can encode mutability, which is a must for anything performance oriented. That is a benefit that FP misses out on. You can still analyze Rust programs with a great deal of assurances. The fact that it’s procedural seems to not matter much at all. An example of a language that allows mutability and has a research-level type system is Flix.
  - zelphirkalt 1y ago
    > [...] which is a must for anything performance oriented. But that's also not really true. Using functional data structures it is possible to write highly performant software. Check out for example "CppCon 2017: Juan Pedro Bolivar Puente - Postmodern immutable data structures"[1], an impressive talk, in which someone shows their developed editor that can edit huge text files without lag faster than any mainstream editor today. This is enabled by functional data structures. Usage of functional data structures throughout a project also ensures, that parts can be trivially parallelized, which is not true for traditional algorithms, and therefore can easily scale with number of CPUs available. For more on that subject, you might want to watch a few Joe Armstrong talks. Rust achieves type safety by introducing more language concepts like ownership, borrowing, and lifetimes, to formalize, who has access when and how. It also creates things as immutable by default, unless you make use of `mut`. Unfortunately, Rust's philosophy is shared memory and making shared memory access safe, rather than message passing, which is at odds with FP. [1]: https://www.youtube.com/watch?v=sPhpelUfu8Q https://www.youtube.com/watch?v=sPhpelUfu8Q

denismenace 1y ago

I think in the end step by step functional programming will be widely adopted. Concepts that have a strong theory behind them tend to last longer. Similar to how relational databases and SQL are still the gold standard today.

deleted 1y ago
[deleted]
cubefox 1y ago
That seems improbable. Pure functional languages are very unpopular according to TIOBE. In particular, interest in Haskell seems to be in decline. Functional features are mostly just an add-on to programming languages with mutable state. By far the most popular language, Python, doesn't even have static typing.
- bheadmaster 1y ago
  > By far the most popular language, Python, doesn't even have static typing. Arguably, Python is statically typed - it's just that it only has one type: object.
  - wk_end 1y ago
    I know Robert Harper has advanced that argument, but I think it's only really interesting for striking a single rhetorical blow: that, uh, actually statically typed languages are trivially more expressive than Python, since Python has one static type and they have as many as you want. But I think as an actual ontology, as an actual way of understanding and structuring the world, it's obviously quite silly. There's no compile-time (static) type checking phase in Python, because it'd be trivial and therefore a waste of time. Without static type checking, what does it mean to say it's "statically" typed? Moreover, the language has an entirely different, extraordinarily related concept of type which is checked dynamically. Yes, you can say that "Python is a statically typed language with only a single meaningless static type and but also dynamically checked dynamic types", but frankly that's not telling you anything that calling it a dynamically typed language isn't. From a different angle, you can't program SML or something "monotypically" - just restricting yourself to one type - without effectively building an interpreter for an entirely separate, dynamic language inside of it (you can of course build a statically typed language inside of Python, so if you think that counts you're just stripping the meaning from comparing languages). In that sense, Python's just plain doing something fundamentally different from what "a static language with one type" is.

YellowSuB 1y ago

Is this book available in print version anywhere? I am unable to find it except for a used hardcover.

lo_zamoyski 1y ago
It's out-of-print.

deleted 1y ago

[deleted]

phoenixhaber 1y ago

[dead]

bedman12345 1y ago

Man I hate functional programming so much. Please, to anyone reading this. Don’t waste your time on this stuff. They always try to claim functional code makes things safer and more elegant, but I have never seen that in reality. These ideas seem to produce terrible code first and foremost.

jghn 1y ago
Can you provide objective measures for "terrible code" and then examples of what you're describing?
- bedman12345 1y ago
  It’s slow. Example: quicksort [] = [] quicksort (p:xs) = (quicksort lesser) ++ [p] ++ (quicksort greater) where lesser = filter (< p) xs greater = filter (>= p) xs It’s really complicated. Everybody includes lenses https://hackage.haskell.org/package/lens https://hackage.haskell.org/package/lens I don’t want to read all that stuff just for imperative syntax. It’d both slow and hard to read. Compare these two: https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/spectralnorm-ghc-4.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/... https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/spectralnorm-gcc-6.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/... The c examples complexity lies in using SIMD. If you know simd it’s easy. You should know simd, it’s useful. The Haskell example is drivel. Long complicated and in the end hopelessly slow compared to the c example. You could als use simd in Haskell, but then it would just be C with extra steps.
  - jrrv 1y ago
    The Haskell looks much better, and I don't even know Haskell. > If you know simd it’s easy. Surely "if you know Haskell it's easy" is equally applicable.
    - bedman12345 1y ago
      > The Haskell looks much better, and I don't even know Haskell Plain crazy take. The c example uses basic coding to implement some clever maths with special fast instructions. Thehaskell example is just some dumb algo implemented with complicated programming. There is obviously nothing good about that. You can also look at a c example without simd https://benchmarksgame-team.pages.debian.net/benchmarksgame/program/spectralnorm-gcc-3.html https://benchmarksgame-team.pages.debian.net/benchmarksgame/... It’s shorter and simpler and faster than the Haskell version. It’s not even close???