3 ms·

This seems strange to me, but it's hours past my bed time and I haven't tried reading lambda calculus or lambda-star calculus theory in about 20 years. Many pr

This seems strange to me, but it's hours past my bed time and I haven't tried reading lambda calculus or lambda-star calculus theory in about 20 years. Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types. There is some nuance and special cases. Like any null is considered a null instance of any nullable object, but you're also not permitted to ask a null value what type it is. It just is a null. Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class. Presumably the difference is either in one of those nuances, or else in some other axiomatic assertion in the language design that this paper is not making. Or else I'm very much missing what the author is driving at, which at this time of the morning seems equally possible.

lalaithion 8mo ago
System.Object is a type of all objects, NOT a type of all types. That is, all objects are System.Object. If one has a class Foo, then every object of type Foo is also of type System.Object. But what is the type of Foo itself? Not of an instance of Foo, but Foo itself. In the languages this paper is about, the type system can recurse upon itself, allowing types themselves to have type. It’s sort of like C#’s System.Type, except System.Type is a class that holds type information for runtime type inspection, whereas the type of types in this paper is for compile-time generics that can abstract over not just types but the types of types as well.
magicalhippo 8mo ago
> Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class. Incidentally one of the things I missed from Delphi in C#. In Delphi you can declare type TWidgetClass = class of TWidget; Then you can declare variables of TWidgetClass, and assign TWidget or any subclass to such variables, and call class methods using it, like say the constructor. var widgetClass := TTextWidget; var myWidget := widgetClass.Create(); After which myWidget holds and instance of TTextWidget. Very handy for factory pattern code, but also other stuff. Of course after C# got generics it alleviated some of this.
lmm 8mo ago
> Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types. That's a type of all values, not a type of all types. In richer programming languages, you can do operations on types much like you can do operations on values. E.g. in C# you can write "List<String>", but you can't do something like "var x = List; var y = String; x<y>". (Which might seem pointless, but it allows you to do things like write a conversion from x<Int> to x<String> that you can reuse with different x types). So then you need a type for x and y, which is conventionally type, and you have to ask what the type of type is. (And if it's type, then that's very natural and makes some things very easy - but at the cost of making typechecking undecidable, as per the article).
- da_chicken 8mo ago
  No, it's not that. You can actually do those things in C#. You just can't do them at compile time. You have to use introspection or the dynamic keyword and do it at runtime. In order to do what you're suggesting at compile time, you'd need a type of types, and then you'll run into the decidability paradox.

lalaithion 8mo ago

System.Object is a type of all objects, NOT a type of all types. That is, all objects are System.Object. If one has a class Foo, then every object of type Foo is also of type System.Object. But what is the type of Foo itself? Not of an instance of Foo, but Foo itself. In the languages this paper is about, the type system can recurse upon itself, allowing types themselves to have type. It’s sort of like C#’s System.Type, except System.Type is a class that holds type information for runtime type inspection, whereas the type of types in this paper is for compile-time generics that can abstract over not just types but the types of types as well.

magicalhippo 8mo ago

> Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class. Incidentally one of the things I missed from Delphi in C#. In Delphi you can declare type TWidgetClass = class of TWidget; Then you can declare variables of TWidgetClass, and assign TWidget or any subclass to such variables, and call class methods using it, like say the constructor. var widgetClass := TTextWidget; var myWidget := widgetClass.Create(); After which myWidget holds and instance of TTextWidget. Very handy for factory pattern code, but also other stuff. Of course after C# got generics it alleviated some of this.

lmm 8mo ago

> Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types. That's a type of all values, not a type of all types. In richer programming languages, you can do operations on types much like you can do operations on values. E.g. in C# you can write "List<String>", but you can't do something like "var x = List; var y = String; x<y>". (Which might seem pointless, but it allows you to do things like write a conversion from x<Int> to x<String> that you can reuse with different x types). So then you need a type for x and y, which is conventionally type, and you have to ask what the type of type is. (And if it's type, then that's very natural and makes some things very easy - but at the cost of making typechecking undecidable, as per the article).

da_chicken 8mo ago
No, it's not that. You can actually do those things in C#. You just can't do them at compile time. You have to use introspection or the dynamic keyword and do it at runtime. In order to do what you're suggesting at compile time, you'd need a type of types, and then you'll run into the decidability paradox.