Ed: actually, Typescript might be a better host for this.
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
So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.
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.
Python does this.
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-lan...
If I write a well-typed function in one of these languages that consumes a value of type Foo, it's statically guaranteed that it can operate on any value of type Foo, regardless of its class, but it needs to dynamically ascertain - using a pattern match - which class of Foo-typed values it is to do anything meaningful with it.
Java operates under the same principle, in its way. In Java, barring escape hatches from the type system (casts), if I write a method that consumes an object of type Foo, likewise, it's statically enforced that it can operate on any object of type Foo, and notably it can't operate on any object of type Object. But in order to invoke a method on my Foo-typed object, it needs to do a dynamic dispatch to ascertain which class' methods to invoke. So what Java calls classes do type-theoretic double-duty - in a static dispatch context, Foo is a type; but in a dynamic dispatch context, Foo's subclasses constitute its open set of (type-theoretic) classes.
This is totally normal nomenclature in PLT circles (Harper, after all, is one of the biggest names in PLT circles, and he's borrowed this idea from Dana Scott who's another big name). The comments section of an article on a programming language, especially one deeply rooted in PLT, is probably a reasonable place to be open to it.
According to this, there are no such things as dynamically typed langugages, only “unityped” ones. I stand by my claim that the former is a normal accepted term, while the latter is niche at best.
Bingo.
That's exactly what Harper said.
Did you actually read that thing?
And (bringing this back to its origin), using terms which actually are in common use, Python does allow storing types as values in variables.
That's the fun thing about it. But in some circles everybody knows this term. ;-) (You can see it as an "in joke", if you like).
> Python does allow storing types as values in variables.
Python does not have "types" in the CS sense (besides the one all mighty uni-type, of course).
All you can store in variables in Python are values. (Before arguing further please look up type theory first, so we can avoid going in circles).
Types in the context of dependent types mean solely static types.
Runtime "types" are not types at all. They're runtime values.
Thanks, much appreciated!
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…
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?
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.)
But unfortunately, there's a lot of work left kind of half-baked so using the language is a pain... if someone invested a lot of time to make Terra work properly and added some tooling around it, wrote proper docs and so on, it would be a really interesting language.
But then Terra doesn’t do that. Lua does. But not to itself, so it’s not really about passing around types as first-class values any more than metaprogramming Java in Python would elevate Java types to being first-class values.
In Zig, you do the metaprogramming in Zig itself, but you're also limited somewhat as you can only use the comptime "layer" of the program. In my mind, it's very similar.
Zig is just doing "compile time reflection". That's not even remotely close to dependent types.
The whole point of DT is that computed types can be used for type checking, and not only to compute values form them.
DT enable to reason about programs as mathematical proves. That's not possible in Zig, afaik.
If merely passing around values called "types" would be similar to what Idris does every language with runtime reflection and also all dynamic(!) languages would have DT. That's of course not true.
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?
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).
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.)
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.
Ecstasy (xtclang).
> 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.
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.
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.
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...