6 ms·

Which programming languages have a strong enough type system to do this? And does it have any draw backs to implement type-level natural numbers, or is it just

Which programming languages have a strong enough type system to do this? And does it have any draw backs to implement type-level natural numbers, or is it just complicated and a lot of work?

tomsmeding 4y ago
Haskell does, and you get decent type-level arithmetic with a compiler plugin.
pharmakom 4y ago
C++ templates (of all things) can do this. This is one reason so many C++ replacements fail. Numbers in templates can be key for performance.
- t8sr 4y ago
  Speaking of replacements, this is my big complaint about Rust's type system - it has no replacement for templates. Instead, it has two ways of doing parametric types like matrices: 1. Using the type system, as seen in e.g. nalgebra (https://docs.rs/nalgebra/latest/nalgebra/base/struct.Matrix.html https://docs.rs/nalgebra/latest/nalgebra/base/struct.Matrix....) 2. Using macros for codegen, as seen in almost all other linear algebra crates, e.g. ultraviolet (https://crates.io/crates/ultraviolet https://crates.io/crates/ultraviolet) The drawback of (1) is that it's hard to understand or extend, and the type errors are insane, and put Boost to shame. The drawback of (2) is that's just a macro. Of course (1) and (2) are not interoperable. C++ templates are really underappreciated, because they are a single mechanism that gives you both powerful generics and macro-like codegen, while being easy to adopt gradually. (E.g. you can add concepts when it gets unwieldy, but you don't have to rewrite the whole thing.)
  - zokier 4y ago
    Rust has const generics these days that bring true type level numbers, so you can have stuff like this let result: Matrix<i32, 2, 2> = matrix_a * matrix_b; https://github.com/MayorMonty/mtrx https://github.com/MayorMonty/mtrx
    - pjmlp 4y ago
      They are still relatively limited versus the HKT from C++ templates.
  - pjmlp 4y ago
    I also find that even though it is a language inside a language, it is much easier to keep track of, because it is uses the same C++ language features instead of a special set of macro operators and semantics.
tmtvl 4y ago
Common Lisp has a very powerful type system, though when it comes to playing around with types you might as well load up Coalton.
- still_grokking 4y ago
  Since when CL is statically typed? LISP has only one type. The all mighty runtime type. It's a uni-typed language.
  - tmtvl 4y ago
    Yeah, I'm sure deftype does nothing. (deftype option (subtype) "The type of a value that is either nil or a value of SUBTYPE." `(or null ,subtype)) (defun* get-latest-statement ((account account)) "If any statements have been made on the ACCOUNT, returns the latest. Otherwise returns nil." (:returns (option statement)) (car (last (account-statements account)))) I like defstar, it's a neat package.
  - andsoitis 4y ago
    The person you replied to didn’t say CL is statically typed. They said “powerful”. While CL (the standard) doesn’t require compile time type checking AFAIK, certain implementations, such as SBCL (probably the most popular non-commercial implementation), does offer compile time type checking. More on CL types, type checking, etc.: https://lispcookbook.github.io/cl-cookbook/type.html https://lispcookbook.github.io/cl-cookbook/type.html
    - still_grokking 4y ago
      > They said “powerful”. Yes, it was called a "powerful type system". But a type system with only one type isn't powerful, more the contrary. https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan... But the now linked page was an interesting read. At least SBCL has indeed real types. I didn't know that until now. Compile-time type checking You may provide type information for variables, function arguments etc via `proclaim`, `declaim` and `declare`. However, similar to the `:type` slot introduced in CLOS section, the effects of type declarations are undefined in Lisp standard and are implementation specific. So there is no guarantee that the Lisp compiler will perform compile-time type checking. However, it is possible, and SBCL is an implementation that does thorough type checking.
mananaysiempre 4y ago
The drawback is that if you also have (parametric) polymorphism (and you do, unless you’re strictly standard Pascal and impossible to write libraries in), your typechecker now needs to answer arbitrary questions of the form “are there natural numbers that make this equality true?” in order to tell if something is well-typed or not. And that is of course impossible in general (per Gödel and Turing), so now it’s one on you to give the proofs. So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems and, though it’s perfectly possible to write useful programs in them, it requires a more disciplined and restricted approach than usual, and you’re going have to spend some time proving things. There are also languages—notably C++ and Haskell—that do this less seriously, in that their systems are capable of expressing naturals but are either unsound (allowing some programs that passed the typechecker to misbehave due to type-related problems), semidecidable (allowing the typechecker to hang on erroneous programs), too weak (not allowing you to prove equalities you need), or all of the above. On the upside, those are also the ones flexible enough that normal people can program in them (as long as they don’t try typing every length and size they see, then it becomes as painful as ever). (Other responses have mentioned interesting type systems for dynamic languages, such as those in Racket and Common Lisp. I think those mostly fall into the “unsound” bucket above, due to runtime checks, but I don’t know much about them. Should be worth looking into as well.)
- biorach 4y ago
  > So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right?
  - xavxav 4y ago
    Both, but almost more importantly the languages themselves are all strictly terminating. Long story short, these languages are based on the “Howard-Curry isomorphism” which says that we can view type signatures as theorems and programs with that signature proofs of that theorem. A program which runs forever is a proof of false (you could see it as saying “after infinity time I’ll have your answer I swear”). So these languages are designed to prevent that from being possible.
still_grokking 4y ago
> Which programming languages have a strong enough type system to do this? Besides the other mentions Scala 3 has type level arithmetic built in. Quick peek: https://gist.github.com/deanwampler/b1176dc939abc092681368c9aa8dafb5#file-scala3-DependentTypes-IntAlgebra-scala https://gist.github.com/deanwampler/b1176dc939abc092681368c9... You could do things like that also in Scala 2. But the code to make it work would be quite involved.
dang 4y ago
Sorry for offtopicness, but could you please email hn@ycombinator.com? I want to send you a repost invite.

Which programming languages have a strong enough type system to do this? And does it have any draw backs to implement type-level natural numbers, or is it just complicated and a lot of work?

tomsmeding 4y ago

Haskell does, and you get decent type-level arithmetic with a compiler plugin.

pharmakom 4y ago

C++ templates (of all things) can do this. This is one reason so many C++ replacements fail. Numbers in templates can be key for performance.

t8sr 4y ago
Speaking of replacements, this is my big complaint about Rust's type system - it has no replacement for templates. Instead, it has two ways of doing parametric types like matrices: 1. Using the type system, as seen in e.g. nalgebra (https://docs.rs/nalgebra/latest/nalgebra/base/struct.Matrix.html https://docs.rs/nalgebra/latest/nalgebra/base/struct.Matrix....) 2. Using macros for codegen, as seen in almost all other linear algebra crates, e.g. ultraviolet (https://crates.io/crates/ultraviolet https://crates.io/crates/ultraviolet) The drawback of (1) is that it's hard to understand or extend, and the type errors are insane, and put Boost to shame. The drawback of (2) is that's just a macro. Of course (1) and (2) are not interoperable. C++ templates are really underappreciated, because they are a single mechanism that gives you both powerful generics and macro-like codegen, while being easy to adopt gradually. (E.g. you can add concepts when it gets unwieldy, but you don't have to rewrite the whole thing.)
- zokier 4y ago
  Rust has const generics these days that bring true type level numbers, so you can have stuff like this let result: Matrix<i32, 2, 2> = matrix_a * matrix_b; https://github.com/MayorMonty/mtrx https://github.com/MayorMonty/mtrx
  - pjmlp 4y ago
    They are still relatively limited versus the HKT from C++ templates.
- pjmlp 4y ago
  I also find that even though it is a language inside a language, it is much easier to keep track of, because it is uses the same C++ language features instead of a special set of macro operators and semantics.

tmtvl 4y ago

Common Lisp has a very powerful type system, though when it comes to playing around with types you might as well load up Coalton.

still_grokking 4y ago
Since when CL is statically typed? LISP has only one type. The all mighty runtime type. It's a uni-typed language.
- tmtvl 4y ago
  Yeah, I'm sure deftype does nothing. (deftype option (subtype) "The type of a value that is either nil or a value of SUBTYPE." `(or null ,subtype)) (defun* get-latest-statement ((account account)) "If any statements have been made on the ACCOUNT, returns the latest. Otherwise returns nil." (:returns (option statement)) (car (last (account-statements account)))) I like defstar, it's a neat package.
- andsoitis 4y ago
  The person you replied to didn’t say CL is statically typed. They said “powerful”. While CL (the standard) doesn’t require compile time type checking AFAIK, certain implementations, such as SBCL (probably the most popular non-commercial implementation), does offer compile time type checking. More on CL types, type checking, etc.: https://lispcookbook.github.io/cl-cookbook/type.html https://lispcookbook.github.io/cl-cookbook/type.html
  - still_grokking 4y ago
    > They said “powerful”. Yes, it was called a "powerful type system". But a type system with only one type isn't powerful, more the contrary. https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan... But the now linked page was an interesting read. At least SBCL has indeed real types. I didn't know that until now. Compile-time type checking You may provide type information for variables, function arguments etc via `proclaim`, `declaim` and `declare`. However, similar to the `:type` slot introduced in CLOS section, the effects of type declarations are undefined in Lisp standard and are implementation specific. So there is no guarantee that the Lisp compiler will perform compile-time type checking. However, it is possible, and SBCL is an implementation that does thorough type checking.

mananaysiempre 4y ago

The drawback is that if you also have (parametric) polymorphism (and you do, unless you’re strictly standard Pascal and impossible to write libraries in), your typechecker now needs to answer arbitrary questions of the form “are there natural numbers that make this equality true?” in order to tell if something is well-typed or not. And that is of course impossible in general (per Gödel and Turing), so now it’s one on you to give the proofs. So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems and, though it’s perfectly possible to write useful programs in them, it requires a more disciplined and restricted approach than usual, and you’re going have to spend some time proving things. There are also languages—notably C++ and Haskell—that do this less seriously, in that their systems are capable of expressing naturals but are either unsound (allowing some programs that passed the typechecker to misbehave due to type-related problems), semidecidable (allowing the typechecker to hang on erroneous programs), too weak (not allowing you to prove equalities you need), or all of the above. On the upside, those are also the ones flexible enough that normal people can program in them (as long as they don’t try typing every length and size they see, then it becomes as painful as ever). (Other responses have mentioned interesting type systems for dynamic languages, such as those in Racket and Common Lisp. I think those mostly fall into the “unsound” bucket above, due to runtime checks, but I don’t know much about them. Should be worth looking into as well.)

biorach 4y ago
> So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right?
- xavxav 4y ago
  Both, but almost more importantly the languages themselves are all strictly terminating. Long story short, these languages are based on the “Howard-Curry isomorphism” which says that we can view type signatures as theorems and programs with that signature proofs of that theorem. A program which runs forever is a proof of false (you could see it as saying “after infinity time I’ll have your answer I swear”). So these languages are designed to prevent that from being possible.

still_grokking 4y ago

> Which programming languages have a strong enough type system to do this? Besides the other mentions Scala 3 has type level arithmetic built in. Quick peek: https://gist.github.com/deanwampler/b1176dc939abc092681368c9aa8dafb5#file-scala3-DependentTypes-IntAlgebra-scala https://gist.github.com/deanwampler/b1176dc939abc092681368c9... You could do things like that also in Scala 2. But the code to make it work would be quite involved.

dang 4y ago

Sorry for offtopicness, but could you please email hn@ycombinator.com? I want to send you a repost invite.