7 ms·

>"In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like a

>"In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This is a small but powerful idea, enabling: o Relationships to be expressed between values; for example, that two lists have the same length. o Assumptions to be made explicit and checked by the compiler. For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. o If desired, properties of program behaviour to be formally stated and proven." PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs...

kitd 4y ago
This is presumably not what you're thinking of but ofc Javascript uses objects as prototype "types". As is, they wont provide what you want, but if there was some kind of "compile-time" processing of prototypes such that types assemblies, dependencies, constraints and other relationships could be manipulated or asserted before they were applied in runtime code, that may provide some of the "first-class type" functionality mentioned. Ed: actually, Typescript might be a better host for this.
- eckza 4y ago
  FP Or Die Gang is downvoting you, but this is actually correct. No referential transparency (among other things, no doubt) makes this a harder problem to solve than just using a language that supports it. $0.02
  - still_grokking 4y ago
    If you don't have referential transparency mathematical equations don't hold. You can't be sure that `a = b` stays true if deducted once. So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.
    - eckza 4y ago
      Thank you for this. That's exactly what I was getting at; you illustrated it far better.
- still_grokking 4y ago
  The down-votes are likely because the example isn't anyhow good. But the idea to have static prototype types is imho quite interesting on its own. I was thinking a lot about that in the past. I would love to have JS like objects—but in a static context. Row polymorphism and extensible records are close but still not there actually.
teddyh 4y ago
> PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Python does this.
- ihm 4y ago
  These types are statically checked (i.e., can be checked before runtime).
  - teddyh 4y ago
    I was not replying to the article, I was replying to the question from “peter_d_sherman” asking if any other programming language has types as first-class constructs. And Python does that.
    - peter_d_sherman 4y ago
      Sure! I'll accept Python into the list of languages that have types as first-class constructs! And thanks, the suggestion is much appreciated!
    - typedfalse 4y ago
      Eh, in this context those aren't types; instead Python is unityped. Agreed they are still fun though.
      - xigoi 4y ago
        Python is dynamically typed, but definitely not untyped.
        wk_end 4y ago
        typedfalse wrote "unityped", not "untyped" (note the "i"). When type system people talk about types they're implicitly talking about static types, rather than what Python might call a type. Robert Harper lays out the argument [0] that Python is basically a statically typed language with many "classes" but a single type - that's where I was first exposed to this idea. > The characteristics of a dynamic language are [that] values are classified [...] into a variety of forms that can be distinguished at run-time. A collection of values can be of a variety of classes, and we can sort out at run-time which is which and how to handle each form of value. Since every value in a dynamic language is classified in this manner, what we are doing is agglomerating all of the values of the language into a single, gigantic (perhaps even extensible) type. To borrow an apt description from Dana Scott, the so-called untyped (that is “dynamically typed”) languages are, in fact, unityped. Rather than have a variety of types from which to choose, there is but one! > And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer. Conceptually, this is just rubbish, but it has serious, tangible penalties. For one, you are depriving yourself of the ability to state and enforce the invariant that the value at a particular program point must be an integer. For another, you are imposing a serious bit of run-time overhead to represent the class itself (a tag of some sort) and to check and remove and apply the class tag on the value each time it is used. [0] https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
ihm 4y ago
The most famous ones off the top of my head: Coq, Agda, Lean, Idris, ATS. Here's a list: https://en.wikipedia.org/wiki/Category:Dependently_typed_languages https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...
- peter_d_sherman 4y ago
  That (and pages like that) are what I was looking for! Thanks, much appreciated!
  - still_grokking 4y ago
    Scala is missing on that list (even it doesn't have "full dependent types" Match-Types are quite close).
- eggy 4y ago
  I tried ATS after finding Rust difficult. Zig is becoming my C replacement, and ATS is like a C++ replacement, although, I am using SPARK2014 now, but I am looking into ATS' contracts. There is no lack of PLs as a tool for whatever you may need to do nowadays. It's refreshing compared to 1970s to 1980s for me.
deleted 4y ago
[deleted]
csande17 4y ago
Zig is probably the closest you'll get to this in an imperative language. You can write functions that take types as arguments and return types, and that's how e.g. generic data structures are implemented.
- astrange 4y ago
  You can do that in Smalltalk descendants, if by types you mean metaclasses.
  - still_grokking 4y ago
    No, types are not runtime values! That's the whole point. That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker. At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…
    - astrange 4y ago
      "Runtime value" is an implementation detail. You could write an Idris interpreter. It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?
      - still_grokking 4y ago
        > "Runtime value" is an implementation detail. You could write an Idris interpreter. Sure. And such an interpreter would still not interpret types at runtime, as types are not (runtime) values. Only at type-checking time (which is of course a phase before the program actually runs / gets interpreted) you would do anything with the types. > It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error? Whether that would be anyhow "useful" depends on the definition of "file usage". If there's any reference form the "used" parts of the program to the "unused file" you have a problem: A type error (in a language where "programs as proves" is a thing) means that you "proved" false. But form a "prove" of false you can "prove" anything! So you actually lost all proving power. Your program may now explode at runtime with arbitrary type errors anywhere. At that point your "static type system" becomes completely useless. (Of course, if nothing in your "unused file" is referenced anywhere in the "used" files, noting happens. But in this case that "unused file" isn't part of your program, so it's completely irrelevant what's inside anyway.)
skybrian 4y ago
Zig does some of this. Functions can be written that can be called at compile time or runtime, depending on which language features they use. Types can be computed and returned by functions in compile-time expressions. I don't know how expressive the types can get, though?
- Avshalom 4y ago
  I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.
- still_grokking 4y ago
  You can pass "types" also around in C#… But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).
  - skybrian 4y ago
    The types created in compile-time code are just as "real" as the types you declare in source code. All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator. (Reflective use of runtime types in languages like C#, Java, or Go is different.)
    - still_grokking 4y ago
      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.
cpurdy 4y ago
>I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Ecstasy (xtclang).
still_grokking 4y ago
The examples are completely out of context. > Relationships to be expressed between values; for example, that two lists have the same length. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. You don't need types for that at all… > Assumptions to be made explicit and checked by the compiler. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. In theory you don't need types for that at all. (Even types would be the current std. method to achieve that). > For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. You can construct a NEL (NonEmptyList) in any language. That's trivial. You just need to enforce the usage of the right factory method for your list. > If desired, properties of program behaviour to be formally stated and proven. This has nothing to do with dependent types (directly). A language based on simply typed lambda calculus is "enough" to arrive at this property.
- dmytrish 4y ago
  Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.
  - still_grokking 4y ago
    Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.

kitd 4y ago

This is presumably not what you're thinking of but ofc Javascript uses objects as prototype "types". As is, they wont provide what you want, but if there was some kind of "compile-time" processing of prototypes such that types assemblies, dependencies, constraints and other relationships could be manipulated or asserted before they were applied in runtime code, that may provide some of the "first-class type" functionality mentioned. Ed: actually, Typescript might be a better host for this.

eckza 4y ago
FP Or Die Gang is downvoting you, but this is actually correct. No referential transparency (among other things, no doubt) makes this a harder problem to solve than just using a language that supports it. $0.02
- still_grokking 4y ago
  If you don't have referential transparency mathematical equations don't hold. You can't be sure that `a = b` stays true if deducted once. So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.
  - eckza 4y ago
    Thank you for this. That's exactly what I was getting at; you illustrated it far better.
still_grokking 4y ago
The down-votes are likely because the example isn't anyhow good. But the idea to have static prototype types is imho quite interesting on its own. I was thinking a lot about that in the past. I would love to have JS like objects—but in a static context. Row polymorphism and extensible records are close but still not there actually.

teddyh 4y ago

> PDS: I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Python does this.

ihm 4y ago
These types are statically checked (i.e., can be checked before runtime).
- teddyh 4y ago
  I was not replying to the article, I was replying to the question from “peter_d_sherman” asking if any other programming language has types as first-class constructs. And Python does that.
  - peter_d_sherman 4y ago
    Sure! I'll accept Python into the list of languages that have types as first-class constructs! And thanks, the suggestion is much appreciated!
  - typedfalse 4y ago
    Eh, in this context those aren't types; instead Python is unityped. Agreed they are still fun though.
    - xigoi 4y ago
      Python is dynamically typed, but definitely not untyped.
      - wk_end 4y ago
        typedfalse wrote "unityped", not "untyped" (note the "i"). When type system people talk about types they're implicitly talking about static types, rather than what Python might call a type. Robert Harper lays out the argument [0] that Python is basically a statically typed language with many "classes" but a single type - that's where I was first exposed to this idea. > The characteristics of a dynamic language are [that] values are classified [...] into a variety of forms that can be distinguished at run-time. A collection of values can be of a variety of classes, and we can sort out at run-time which is which and how to handle each form of value. Since every value in a dynamic language is classified in this manner, what we are doing is agglomerating all of the values of the language into a single, gigantic (perhaps even extensible) type. To borrow an apt description from Dana Scott, the so-called untyped (that is “dynamically typed”) languages are, in fact, unityped. Rather than have a variety of types from which to choose, there is but one! > And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer. Conceptually, this is just rubbish, but it has serious, tangible penalties. For one, you are depriving yourself of the ability to state and enforce the invariant that the value at a particular program point must be an integer. For another, you are imposing a serious bit of run-time overhead to represent the class itself (a tag of some sort) and to check and remove and apply the class tag on the value each time it is used. [0] https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...

ihm 4y ago

The most famous ones off the top of my head: Coq, Agda, Lean, Idris, ATS. Here's a list: https://en.wikipedia.org/wiki/Category:Dependently_typed_languages https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...

peter_d_sherman 4y ago
That (and pages like that) are what I was looking for! Thanks, much appreciated!
- still_grokking 4y ago
  Scala is missing on that list (even it doesn't have "full dependent types" Match-Types are quite close).
eggy 4y ago
I tried ATS after finding Rust difficult. Zig is becoming my C replacement, and ATS is like a C++ replacement, although, I am using SPARK2014 now, but I am looking into ATS' contracts. There is no lack of PLs as a tool for whatever you may need to do nowadays. It's refreshing compared to 1970s to 1980s for me.

deleted 4y ago

[deleted]

csande17 4y ago

Zig is probably the closest you'll get to this in an imperative language. You can write functions that take types as arguments and return types, and that's how e.g. generic data structures are implemented.

astrange 4y ago
You can do that in Smalltalk descendants, if by types you mean metaclasses.
- still_grokking 4y ago
  No, types are not runtime values! That's the whole point. That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker. At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…
  - astrange 4y ago
    "Runtime value" is an implementation detail. You could write an Idris interpreter. It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?
    - still_grokking 4y ago
      > "Runtime value" is an implementation detail. You could write an Idris interpreter. Sure. And such an interpreter would still not interpret types at runtime, as types are not (runtime) values. Only at type-checking time (which is of course a phase before the program actually runs / gets interpreted) you would do anything with the types. > It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error? Whether that would be anyhow "useful" depends on the definition of "file usage". If there's any reference form the "used" parts of the program to the "unused file" you have a problem: A type error (in a language where "programs as proves" is a thing) means that you "proved" false. But form a "prove" of false you can "prove" anything! So you actually lost all proving power. Your program may now explode at runtime with arbitrary type errors anywhere. At that point your "static type system" becomes completely useless. (Of course, if nothing in your "unused file" is referenced anywhere in the "used" files, noting happens. But in this case that "unused file" isn't part of your program, so it's completely irrelevant what's inside anyway.)

skybrian 4y ago

Zig does some of this. Functions can be written that can be called at compile time or runtime, depending on which language features they use. Types can be computed and returned by functions in compile-time expressions. I don't know how expressive the types can get, though?

Avshalom 4y ago
I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.
still_grokking 4y ago
You can pass "types" also around in C#… But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).
- skybrian 4y ago
  The types created in compile-time code are just as "real" as the types you declare in source code. All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator. (Reflective use of runtime types in languages like C#, Java, or Go is different.)
  - still_grokking 4y ago
    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.

cpurdy 4y ago

>I'd be curious to know about any/all languages where types can be passed to functions, returned from functions -- and even generated at runtime by functions... that is, where the language regards types as first-class constructs... Ecstasy (xtclang).

still_grokking 4y ago

The examples are completely out of context. > Relationships to be expressed between values; for example, that two lists have the same length. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. You don't need types for that at all… > Assumptions to be made explicit and checked by the compiler. This can be also expressed in any language, even in unityped (a.k.a. "dynamic") ones. In theory you don't need types for that at all. (Even types would be the current std. method to achieve that). > For example, if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run. You can construct a NEL (NonEmptyList) in any language. That's trivial. You just need to enforce the usage of the right factory method for your list. > If desired, properties of program behaviour to be formally stated and proven. This has nothing to do with dependent types (directly). A language based on simply typed lambda calculus is "enough" to arrive at this property.

dmytrish 4y ago
Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.
- still_grokking 4y ago
  Of course. But the examples given missed the point imho. All of the stated things don't need any type level machinery. You can just test things at runtime and be good. If you want to prove things at compile time that's a very different story. But than this needs to be explicitly stated in the examples.