7 ms·

Functional Typelevel Programming in Scala

70 points by nuriaion 8y ago

noncoml 8y ago
> Consider the standard definition of typelevel Peano numbers. > A function that maps positive integers to Peano numbers can be defined as follows Really? That was the simplest example you could think of?
- imh 8y ago
  Peano numbers are kind of a classic first typelevel programming example. Maybe it's their unofficial Hello World. Booleans and natural numbers are usually the start, but natural numbers are complex enough to show the pain points.
- type_enthusiast 8y ago
  As a shapeless enthusiast I agree with you that the Peano examples (which seem to be the go-to for any dependent types demo; not just for Scala... they must think it's helpful!) is terrible for people who don't already get dependent typing and logic programming. Which are the people you're supposed to be reaching with a demo. I have a talk to intro typelevel proofs in Scala (with shapeless as the example target), that uses the kind of geometric proofs we all did in high school as an analogy. I think that's more of an accessible metaphor, but it also seems like precisely what Odersky is trying to eliminate in Dotty - the use of inductive implicit derivation to form "proofs" of invariants that are also implementations. Admittedly, it's an approach that seems rather difficult for a lot of engineers to grasp, which means it's of questionable utility. But it always seemed really elegant to me - type systems are about proving invariants, and Scala's just gives you powerful ways to prove things by unifying that concept into implicits.
  - rs86 8y ago
    Yep, it's hard to grasp for engineers, this kind of thing requires training in formal logics to get started with. I think things will not make much sense until one gets that the type system can be a formal system equivalent to logic
didibus 8y ago
I've never heard of typelevel programming. Can someone explain what it is?
- Joeri 8y ago
  I haven’t done it myself, but I understand it as creatively using the type system to have the compiler already partially evaluate the program, instead of deferring all execution to runtime as with traditional programming.
  - chowells 8y ago
    It's usually more about adding additional constraints on code that the type checker will accept than it is about partial evaluation. That is, you're embedding additional logic in the type system. This additional logic lets you be more precise about what operations are allowed on values of particular types. It's most useful when there are additional facilities in the language for type-directed code generation, at which point the complex types can also be used to generate behavior, not just restrict it. (Some examples of type-directed code generation include traits in Rust, implicits in Scala, and type classes in Haskell.)
    - lomnakkus 8y ago
      I think you may be thinking more about typeful programming? (Aka. type-driven design.) At least to me type-level programming is just a mechanism to achieve more at compile time. Another mechanism would be e.g. C++ constexpr or dependent types as in e.g. Idris.
      - chowells 8y ago
        No, I definitely mean type-level programming. Sure, most dependent typing systems subsume type-level programming, but you can do interesting things without needing dependent types. The only requirement for type-level programming is that you have program logic that functions at the type level, taking types as arguments and returning a type. The most overused common example is concatenation of length-indexed vector types. You need a type-level addition function in order for that to be expressible. A more sophisticated example where type-driven code generation is required would be something like a type-safe printf that puts the format string at the type level and computes the required argument types from it at compile time. Sure, you can stuff entire programs into the type level, but that's not where things are the most useful. The greatest value comes from using type-level functions to make the types describing your values more precise.
virtualwhys 8y ago
Looks like this[1] could eliminate quite a bit of typeclass boilerplate. And this[2] opens the door for typed literals in Scala (which are quite a nice feature in TypeScript). Will be interesting to see what use cases library authors apply TLP to in Dotty/Scala 3. [1] https://github.com/dotty-staging/dotty/blob/add-transparent/docs/docs/typelevel.md https://github.com/dotty-staging/dotty/blob/add-transparent/... [2] https://github.com/dotty-staging/dotty/blob/add-transparent/docs/docs/typelevel.md https://github.com/dotty-staging/dotty/blob/add-transparent/...

70 points by nuriaion 8y ago

> Consider the standard definition of typelevel Peano numbers. > A function that maps positive integers to Peano numbers can be defined as follows Really? That was the simplest example you could think of?

imh 8y ago
Peano numbers are kind of a classic first typelevel programming example. Maybe it's their unofficial Hello World. Booleans and natural numbers are usually the start, but natural numbers are complex enough to show the pain points.
type_enthusiast 8y ago
As a shapeless enthusiast I agree with you that the Peano examples (which seem to be the go-to for any dependent types demo; not just for Scala... they must think it's helpful!) is terrible for people who don't already get dependent typing and logic programming. Which are the people you're supposed to be reaching with a demo. I have a talk to intro typelevel proofs in Scala (with shapeless as the example target), that uses the kind of geometric proofs we all did in high school as an analogy. I think that's more of an accessible metaphor, but it also seems like precisely what Odersky is trying to eliminate in Dotty - the use of inductive implicit derivation to form "proofs" of invariants that are also implementations. Admittedly, it's an approach that seems rather difficult for a lot of engineers to grasp, which means it's of questionable utility. But it always seemed really elegant to me - type systems are about proving invariants, and Scala's just gives you powerful ways to prove things by unifying that concept into implicits.
- rs86 8y ago
  Yep, it's hard to grasp for engineers, this kind of thing requires training in formal logics to get started with. I think things will not make much sense until one gets that the type system can be a formal system equivalent to logic

didibus 8y ago

I've never heard of typelevel programming. Can someone explain what it is?

Joeri 8y ago
I haven’t done it myself, but I understand it as creatively using the type system to have the compiler already partially evaluate the program, instead of deferring all execution to runtime as with traditional programming.
- chowells 8y ago
  It's usually more about adding additional constraints on code that the type checker will accept than it is about partial evaluation. That is, you're embedding additional logic in the type system. This additional logic lets you be more precise about what operations are allowed on values of particular types. It's most useful when there are additional facilities in the language for type-directed code generation, at which point the complex types can also be used to generate behavior, not just restrict it. (Some examples of type-directed code generation include traits in Rust, implicits in Scala, and type classes in Haskell.)
  - lomnakkus 8y ago
    I think you may be thinking more about typeful programming? (Aka. type-driven design.) At least to me type-level programming is just a mechanism to achieve more at compile time. Another mechanism would be e.g. C++ constexpr or dependent types as in e.g. Idris.
    - chowells 8y ago
      No, I definitely mean type-level programming. Sure, most dependent typing systems subsume type-level programming, but you can do interesting things without needing dependent types. The only requirement for type-level programming is that you have program logic that functions at the type level, taking types as arguments and returning a type. The most overused common example is concatenation of length-indexed vector types. You need a type-level addition function in order for that to be expressible. A more sophisticated example where type-driven code generation is required would be something like a type-safe printf that puts the format string at the type level and computes the required argument types from it at compile time. Sure, you can stuff entire programs into the type level, but that's not where things are the most useful. The greatest value comes from using type-level functions to make the types describing your values more precise.

virtualwhys 8y ago

Looks like this[1] could eliminate quite a bit of typeclass boilerplate. And this[2] opens the door for typed literals in Scala (which are quite a nice feature in TypeScript). Will be interesting to see what use cases library authors apply TLP to in Dotty/Scala 3. [1] https://github.com/dotty-staging/dotty/blob/add-transparent/docs/docs/typelevel.md https://github.com/dotty-staging/dotty/blob/add-transparent/... [2] https://github.com/dotty-staging/dotty/blob/add-transparent/docs/docs/typelevel.md https://github.com/dotty-staging/dotty/blob/add-transparent/...