https://blog.klipse.tech/databook/2022/06/22/generic-data-st...
The examples also contradict his other principles, i.e. immutability.
//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;
I guess you mean dependent types[1], but if you don't, I'd appreciate an elaboration. If you do mean DTs, how might it look for a hetero collection?
[1] If anybody has any good intros to dependent typing in C#, that'd be much appreciated. A web search throws up some pretty intimidating stuff.
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
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]
A bit larger example:
void Console.WriteLine(string format, params object[] args);
WriteLine("{%int} {%bool}", ?); // ?'s type is an array with an int value and a boolean value.
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.
(defalias NamedMap
(HMap :mandatory {:first-name Str, :last-name Str}))
(ann full-name [NamedMap -> Str])
(defn full-name [{:keys [first-name last-name]}]
(str first-name " " last-name))
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 }
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:
[
("id", 123),
("content", "..."),
("published", True),
]
-- 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...
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.
there's things you can do to track list length at the type level, but it usually involves putting your data in a special-purpose linked-list thingy: https://docs.idris-lang.org/en/latest/tutorial/typesfuns.htm...
(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[]]
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:
class Foo<T> {
private Foo(...)
static Foo<int> Bar() { ... }
static Foo<string> Zap() { ... }
}
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).
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.