3 ms·

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

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.
  - lomnakkus 8y ago
    Alright, I can see where you're coming from... I guess it does all get kind of fuzzy once you have a TC type system anyway. (Whether that be via full dependent types or the rather strange not-quite-like-working-with-terms-and-types world of not-full-dependent-typing of e.g. Haskell.)
    - dwohnitmok 8y ago
      A Turing-complete type system and a dependent type system are two different and independent things. That is it's possible for a type system to be dependently typed and not Turing complete and it is possible for a type system to be Turing complete and not be dependently typed (even a little bit). Dependent typing concerns whether your types can depend on values. So for example if a then Int else Bool is a (single) dependent type if `a` is a runtime value. The difference between the two can be illustrated with natural numbers with the classic natural-number-indexed vector example that always shows up with dependent typing. If you have a type Vector 5 Character representing a vector of 5 elements of characters, if that 5 is the same 5 as you have at runtime then you have dependent typing. Otherwise this is not an example of dependent types. Put another way, if you're allowed to do something like the following val x: Int = 5 val xs: Vector x Character = Vector('a', 'b', 'c', 'd', 'e') in pseudo-Scala syntax then you have dependent types. If on the other hand you have something like type Zero type One ... type Four type Five ... val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') where you have a special set of type-level numbers that are distinct from your run-time natural numbers then you have typelevel programming but do not have dependent typing. Your type system might let you do arbitrary things with the type-level natural numbers type Zero type One ... which would mean your type system is Turing-complete even if it's not dependently typed. Note that in practice it's usually true that languages with typelevel programming tend to inch towards dependent types. For example, by allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') to type-check but not allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e', 'f') to type-check, unless your language is special-casing behavior for collections, there's usually some way to back out some sort of connection between a type-level Five and a run-time 5 (although this connection often only works for numeric literals in e.g. current Scala and works via macros). There's also a considerable amount of social overlap between programmers interested in typelevel programming and programmers interested in dependent types which tends to drive development of language features along those lines. However, in theory, the two are completely separate.

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.
- lomnakkus 8y ago
  Alright, I can see where you're coming from... I guess it does all get kind of fuzzy once you have a TC type system anyway. (Whether that be via full dependent types or the rather strange not-quite-like-working-with-terms-and-types world of not-full-dependent-typing of e.g. Haskell.)
  - dwohnitmok 8y ago
    A Turing-complete type system and a dependent type system are two different and independent things. That is it's possible for a type system to be dependently typed and not Turing complete and it is possible for a type system to be Turing complete and not be dependently typed (even a little bit). Dependent typing concerns whether your types can depend on values. So for example if a then Int else Bool is a (single) dependent type if `a` is a runtime value. The difference between the two can be illustrated with natural numbers with the classic natural-number-indexed vector example that always shows up with dependent typing. If you have a type Vector 5 Character representing a vector of 5 elements of characters, if that 5 is the same 5 as you have at runtime then you have dependent typing. Otherwise this is not an example of dependent types. Put another way, if you're allowed to do something like the following val x: Int = 5 val xs: Vector x Character = Vector('a', 'b', 'c', 'd', 'e') in pseudo-Scala syntax then you have dependent types. If on the other hand you have something like type Zero type One ... type Four type Five ... val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') where you have a special set of type-level numbers that are distinct from your run-time natural numbers then you have typelevel programming but do not have dependent typing. Your type system might let you do arbitrary things with the type-level natural numbers type Zero type One ... which would mean your type system is Turing-complete even if it's not dependently typed. Note that in practice it's usually true that languages with typelevel programming tend to inch towards dependent types. For example, by allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') to type-check but not allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e', 'f') to type-check, unless your language is special-casing behavior for collections, there's usually some way to back out some sort of connection between a type-level Five and a run-time 5 (although this connection often only works for numeric literals in e.g. current Scala and works via macros). There's also a considerable amount of social overlap between programmers interested in typelevel programming and programmers interested in dependent types which tends to drive development of language features along those lines. However, in theory, the two are completely separate.