Re:Idris: A Language for Type-Driven Development
by still_grokking on Tuesday January 24, 2023 @02:46AM
(#34500694)
Even you almost didn't say anything wrong here there is a key misunderstanding:
The term "type theory", which I've used and to which I referred (and which you've picked up), is a technical term form math.
Languages like C# or Zig are not based on type theory.
What is called "types" in those languages has (mostly) no relation to type theory. Those "types" are (mostly) regular values when looked at them through the type theory lens.
The term "type theory", which I've used and to which I referred (and which you've picked up), is a technical term form math.
Languages like C# or Zig are not based on type theory.
What is called "types" in those languages has (mostly) no relation to type theory. Those "types" are (mostly) regular values when looked at them through the type theory lens.