Awful stuff. These principles could only ever make sense in a dynamic language since it's mostly manually enforcing some of the basic functionality of a type system, but the fact that he also tries to argue this style could be used in a language like C# throws that defense out the window.
It's not impossible to type check heterogeneous maps at compile time, but most static type systems don't support this. I think you'd certainly see much more friction trying to program like this in C# than you would in Clojure.
//Anonymous type with integer property
var foo = new {Number = 1};
//Compile time error if you try to assign a the integer property to a string
string s = foo.Number;
An object is just a fancy map, after all...
These are also immutable by default, which probably makes them even more relevant to this DOA discussion.
Dependent types are types that depend on values, possibly runtime values. In C# types can only depend on other types when using generics: List<T> depends on T.
In C++ there is std::array<T, n> (array with length encoded in type), where n must be known in compile time.
With full dependent types one can write generic types like std::array and use them with runtime parameters.
In dependently-typed languages there are two main types: Sigma (dependent pair) and Pi (dependent function).
Example of Sigma type in pseudo C#:
(uint n, Array<int, n> a); // array of any size
Pi:
Array<T, (n + 1)> push(Type T, uint n, Array<T, n> a, T x) { ... }
Array<int, 3> x = push(int, 2, [1, 2], 3); // [1, 2, 3]
Generic function f<T> is similar to a dependently typed one with `Type T` argument (requires first class types and many DT-langs have them). Values, on which types may depend, shouldn't be mutable, while C# function arguments are mutable.
A bit larger example:
void Console.WriteLine(string format, params object[] args);
Using dependent types you can transform `format` into a heterogeneous array type containing only arguments specified in the format string.
WriteLine("{%int} {%bool}", ?); // ?'s type is an array with an int value and a boolean value.
A heterogeneous map may be implemented as a map T with keys mapped to types and another map where keys are mapped to the values of a corresponding type in T. Probably this is not a good representation, but it is a valid one.
Ouch! But thanks! I'll have a good chew over this evening.
I know it's possible to have DT in C#, I think your literal of '3' in the above example is constructed using the successor function (well, its moral equivalent) at compile time, I just can't find the article I read and there's very little out there for DT in C# at all. And it's over my head until I sit down with a good example and work it through.
I could use some simple DT for list lengths in my project.
siknad and uryga give good replies on dependent types and TypeScript's structural typing. There's also an experimental static typing system for Clojure that allows for typing of maps:
while you probably can do this with dependent types, i'd imagine GP means something along the lines of typescript's structural typing, i.e.
const post = {
id: 123,
content: "...",
published: true,
}
// TS infers the type of `post` to be an unnamed "map-ish" type:
// { id: number, content: string, published: boolean }
JS objects are map-like, and this one is "heterogenous" in that the values are of different types (unlike most maps in statically typed langs, which need to be uniform). this just "structural typing", the easier way to do stuff like this.
now, dependent types allow you to express pretty much arbitrary shapes of data, so you can do heterogenous collections as well. i haven't read about it enough to do a map, but a list of tuples (equivalent if you squint) is "easy" enough:
in Idris, you could type it as something like this:
-- a function describing what type the values of each key are
postKeyValue : String -> Type
postKeyValue k =
case k of
"id" -> Int
"content" -> String
"published" -> Bool
_ -> Void -- i.e. "no other keys allowed"
-- now we're gonna use postKeyValue *at the type level*.
type Post = List (k : String ** postKeyValue k)
-- "a Post is a list of pairs `(key, val)` where the type of each `val` is given by applying `postKeyValue` to `key`.
-- (read `**` like a weird comma, indicating that this is a "dependent pair")
in general if you want to learn more about DT's, i'd probably recommend looking at a language like Idris with "native support" for them. backporting DT's onto an existing typesystem usually makes them much harder to read/understand that they actually are (and don't get me wrong, they're mindbending enough on their own).
if you don't want to bother with that, i'd look at Typescript - it's combination of "literal types", "type guards" and "function overloads" can get you some of the power of DT's. see this article for some examples: https://www.javiercasas.com/articles/typescript-dependent-ty...
Thanks! I guess what you are describing looks - from my very limited experience with scala - as a path-dependent type. If I'm right.
I'm actually talking about C# because I'm working in it and I'd like to make some compile-time guarantees if possible. Or at least know how to assure a method that they are getting a list with at least 2 values in it, for example. It may not be worth the effort but it would be nice to know how.
I've got books on DT, idris, and another DT lang, trouble is there's no call for any of this stuff in industry so they get repeatedly pushed to the bottom of the priority stack. Sickening, innit.
i haven't used scala, but from the looks of it, yeah, "path-dependent types" are a narrow subset of full dependent types, intended for stuff like this exact use case :D
(the `S` and `Z` refer to peano-style natural numbers)
although if you go that way, you can actually get a lot of that without dependent types! here's an example i found of someone doing a similar construction in C#: http://www.javawenti.com/?post=631496
last but not least, in TS you can use the builtin support for arrays as tuples and just do:
type AtLeastTwo<T> = [_1: T, _2: T, ...rest: T[]]
which looks very nice, but it's pretty much only doable because the type system has specific support for array stuff like this, so not a really general solution.
Thanks, yeah, did a big search for DT stuff this morning and found this one. The S/Z is the zero/successor. I need to study it. Perhaps closer to what I originally saw was this https://gist.github.com/bradphelan/26c0e84197092620359a (edit: it's not closer. Still worth a peruse though)
I need to sit and read and butt heads with these if I can find the time.
It's so odd there are so few examples of C# DT. The one good one I found a year ago seems to have disappeared. Maybe a conspiracy?
Looking forward to Idrisizing or Agdicating some time!
another term that might be useful is "GADT" - it's kinda like a weaker form of DT, more easily expressible in, uh, normal languages. the C# one i linked is really more like a GADT, bc it all stays at the type level w/o bringing "normal" values into it. another way to do it would be a sealed class with a private constructor + static methods:
so that way you can have the type param and use it to track something, but limit what can be put there - in this case, only int or string. type-safe syntax trees are a common case for sth like this (though in that case you'd probably go for an abstract base + subclasses, like in the link).
I agree, but I also think if they author either knew what they were talking about or wasn't just trying to sell more books they'd make that clear. Rather than just trying make the case for these patterns in languages that don't suit them.
Kinda funny to say seeing as C# actually has a dynamic type.
Even if you don't use that, you could certainly orient your data as "structs of arrays instead" of "arrays of structs" (so to speak). It's fairly common in games.
https://blog.klipse.tech/databook/2022/06/22/generic-data-st...
The examples also contradict his other principles, i.e. immutability.