4 ms·

For those that are well versed in type theory, what is the neatest solution to this in language design, if there is one at all? I'm always bothered by the ide

by prmph 3y ago

For those that are well versed in type theory, what is the neatest solution to this in language design, if there is one at all? I'm always bothered by the idea that product types can be "more" than, but never "less" than, the type they are assignable to (contra-variance). For sum types it seems to be the opposite (co-variance), so structural typing is easier. Which reminds me of an idea I've had for a while regarding object oriented inheritance. Why is inheritance always approached in a contra-variant manner? I have frequently wished that inheritance could be conceptualized as a narrowing, rather than expansion, of type. For example, consider an "Animal" object class, which has a "numLegs" attribute. Then "Dog" could inherit from "Animal" by having exactly 4 legs, as a special case. I'm not sure whether this concept has been implemented in any language, but I've encountered situations where it would have been the perfect way to model entities, frequently enough, that I believe it could be very useful.

comex 3y ago
I'm not an expert in type theory, but something like Scala's path-dependent types might work. In the following example (which I copy-pasted from [1]), every object of type Foo has some associated type Bar. You can have multiple objects that are all of type Foo, and they might have different Bar types. Therefore, to refer to a Bar type, you have to reference the specific variable you're talking about – such as in "f1.Bar" below, where f1 is a variable name, not a type name. trait Foo{ class Bar def doNothing(b: Bar){} } val f1 = new Foo{} val b1 = new f1.Bar() val f2 = new Foo{} val b2 = new f2.Bar() f1.doNothing(b1) //fine f1.doNothing(b2) //won't compile Applying the same idea to TypeScript, you could imagine using 'keyof' on values instead of types. So instead of keys<T extends object>(o: T): (keyof T)[]; it would be something like keys(o: object): (keyof o)[]; And the keys returned for an object would only let you index into that specific object, not any other object even if it had the same type. [1] https://wheaties.github.io/Presentations/Scala-Dep-Types/dependent-types.html https://wheaties.github.io/Presentations/Scala-Dep-Types/dep...
consilient 3y ago
> For those that are well versed in type theory, what is the neatest solution to this in language design, if there is one at all? Row-polymorphism instead of structural subtyping. The idea is that instead of treating `Record<,>` as parameterized by two ordinary types, you parameterize it with a single type-level collection of key-value pairs, and then write functions which are generic over parts of that collection. So the equivalent of a typescript function that works fine over open records would look something like this `<Rest>(obj: { SomeRow, Rest }) => { SomeRow, Rest }`, whereas `(obj: { SomeRow }) => { SomeRow }` says you can't have any extra entries and `<Rest>(obj: { SomeRow, Rest }) => { SomeRow }` says you can have extra entries but they're getting thrown out. This also lets you reuse machinery between records and sums more easily, since sums are also realizations of rows. Purescript and OCaml have good row type support. You can also sort of hack it together in typescript if you're very very careful, but I wouldn't recommend it.
magicalhippo 3y ago
> For example, consider an "Animal" object class, which has a "numLegs" attribute. Then "Dog" could inherit from "Animal" by having exactly 4 legs, as a special case. In Delphi you can do this: type TAnimal = class abstract public class function NumLegs(): integer; virtual; abstract; end; TDog = class(TAnimal) protected class function NumLegs(): integer; override; end; { TDog } class function TDog.NumLegs: integer; begin result := 4; end; var d: TDog; begin WriteLn(TDog.NumLegs); // 4 d := TDog.Create; WriteLn(d.NumLegs); // 4 end. I've used this several times to good effect. Were you thinking of something else? If so, could you expand a bit?

by prmph 3y ago

comex 3y ago

I'm not an expert in type theory, but something like Scala's path-dependent types might work. In the following example (which I copy-pasted from [1]), every object of type Foo has some associated type Bar. You can have multiple objects that are all of type Foo, and they might have different Bar types. Therefore, to refer to a Bar type, you have to reference the specific variable you're talking about – such as in "f1.Bar" below, where f1 is a variable name, not a type name. trait Foo{ class Bar def doNothing(b: Bar){} } val f1 = new Foo{} val b1 = new f1.Bar() val f2 = new Foo{} val b2 = new f2.Bar() f1.doNothing(b1) //fine f1.doNothing(b2) //won't compile Applying the same idea to TypeScript, you could imagine using 'keyof' on values instead of types. So instead of keys<T extends object>(o: T): (keyof T)[]; it would be something like keys(o: object): (keyof o)[]; And the keys returned for an object would only let you index into that specific object, not any other object even if it had the same type. [1] https://wheaties.github.io/Presentations/Scala-Dep-Types/dependent-types.html https://wheaties.github.io/Presentations/Scala-Dep-Types/dep...

consilient 3y ago

> For those that are well versed in type theory, what is the neatest solution to this in language design, if there is one at all? Row-polymorphism instead of structural subtyping. The idea is that instead of treating `Record<,>` as parameterized by two ordinary types, you parameterize it with a single type-level collection of key-value pairs, and then write functions which are generic over parts of that collection. So the equivalent of a typescript function that works fine over open records would look something like this `<Rest>(obj: { SomeRow, Rest }) => { SomeRow, Rest }`, whereas `(obj: { SomeRow }) => { SomeRow }` says you can't have any extra entries and `<Rest>(obj: { SomeRow, Rest }) => { SomeRow }` says you can have extra entries but they're getting thrown out. This also lets you reuse machinery between records and sums more easily, since sums are also realizations of rows. Purescript and OCaml have good row type support. You can also sort of hack it together in typescript if you're very very careful, but I wouldn't recommend it.

magicalhippo 3y ago

> For example, consider an "Animal" object class, which has a "numLegs" attribute. Then "Dog" could inherit from "Animal" by having exactly 4 legs, as a special case. In Delphi you can do this: type TAnimal = class abstract public class function NumLegs(): integer; virtual; abstract; end; TDog = class(TAnimal) protected class function NumLegs(): integer; override; end; { TDog } class function TDog.NumLegs: integer; begin result := 4; end; var d: TDog; begin WriteLn(TDog.NumLegs); // 4 d := TDog.Create; WriteLn(d.NumLegs); // 4 end. I've used this several times to good effect. Were you thinking of something else? If so, could you expand a bit?