5 ms·

It feels somewhat disingenuous to include a turing-complete meta-programming language (i.e macros) in your definition of the C++ type system. Because vanilla O

It feels somewhat disingenuous to include a turing-complete meta-programming language (i.e macros) in your definition of the C++ type system. Because vanilla OCaml doesn't have any mechanism for expressing compile-time computations, the same level of transformations aren't possible, but I wouldn't call this a limitation of the type-system, rather the meta-programming capabilities. Although, you can somewhat approximate it with modules and functors: module type M = sig type t val t: t end let my_type (type a) (v: a) : (module M) = let module M = struct type t = a let t = v end in (module M : M) module T1 = (val my_type 123) type t1 = T1.t let val1 : t1 = T1.t module T2 = (val my_type val1) type t2 = T2.t

jcelerier 5y ago
> It feels somewhat disingenuous to include a turing-complete meta-programming language (i.e macros) in your definition of the C++ type system. But this is literally what a type system is about ? TS definitions don't care about compile-time and run-time ; what you call "macros" are type-level functions which are a byproduct of the expressivity of C++'s TS. Remember that expressivity of a type system is just the cardinality of the type set you can express with it. Type systems where you can parametrize on nothing are less expressive than type systems that can parametrize on types, which are less expressive than TS which can parametrize on meta-types, which are less expressive than TS which can parametrize on meta-types and integers (C++98, Haskell afaik), which are less expressive than TS which can parametrize on meta-types and arbitrary compile-time values (C++20, soon Rust I believe ?), which I'd guess are less expressive than full-blown dependent types but I'd need to check the exact definition
- pjmlp 5y ago
  Actually you can extend OCaml with similar mechanisms via ppx, apparently op isn't aware of it. https://ocamlverse.github.io/content/metaprogramming.html https://ocamlverse.github.io/content/metaprogramming.html
  - jcelerier 5y ago
    TIL about it, last time I wrote some OCaml camlp4 was still all the rage
    - pjmlp 5y ago
      Yeah, it was decided to merge efforts and integrate into the compiler around the time the Real World OCaml book came out.
- carnitine 5y ago
  Where does that definition of expressivity come from? As far as I can tell the cardinality of the ‘type set’ is omega_0 in both C++ and OCaml.
- bradrn 5y ago
  > TS which can parametrize on meta-types and integers (C++98, Haskell afaik) Haskell also supports type-level strings and type errors, as well as arbitrary ADTs if defined with the -XDataKinds extension enabled. Not sure what you mean by ‘parametrizing on meta-types’ though.

jcelerier 5y ago

> It feels somewhat disingenuous to include a turing-complete meta-programming language (i.e macros) in your definition of the C++ type system. But this is literally what a type system is about ? TS definitions don't care about compile-time and run-time ; what you call "macros" are type-level functions which are a byproduct of the expressivity of C++'s TS. Remember that expressivity of a type system is just the cardinality of the type set you can express with it. Type systems where you can parametrize on nothing are less expressive than type systems that can parametrize on types, which are less expressive than TS which can parametrize on meta-types, which are less expressive than TS which can parametrize on meta-types and integers (C++98, Haskell afaik), which are less expressive than TS which can parametrize on meta-types and arbitrary compile-time values (C++20, soon Rust I believe ?), which I'd guess are less expressive than full-blown dependent types but I'd need to check the exact definition

pjmlp 5y ago
Actually you can extend OCaml with similar mechanisms via ppx, apparently op isn't aware of it. https://ocamlverse.github.io/content/metaprogramming.html https://ocamlverse.github.io/content/metaprogramming.html
- jcelerier 5y ago
  TIL about it, last time I wrote some OCaml camlp4 was still all the rage
  - pjmlp 5y ago
    Yeah, it was decided to merge efforts and integrate into the compiler around the time the Real World OCaml book came out.
carnitine 5y ago
Where does that definition of expressivity come from? As far as I can tell the cardinality of the ‘type set’ is omega_0 in both C++ and OCaml.
bradrn 5y ago
> TS which can parametrize on meta-types and integers (C++98, Haskell afaik) Haskell also supports type-level strings and type errors, as well as arbitrary ADTs if defined with the -XDataKinds extension enabled. Not sure what you mean by ‘parametrizing on meta-types’ though.