Really like this presentation of DOT calculi by and : infoscience.epfl.ch/record/227176/
Covers lots of things that feel _right_ to me: Unifying modules/objects, desugaring type-constructors to modules, intersection & union types, subtyping, type ranges, etc.
Conversation
Glad you like it!
1
I hope your work leads me to someday revisit this tweet:
twitter.com/BrandonBloom/s
Somewhere down that thread there was an interesting discussion with and .
Quote Tweet
I have not encountered a design for generics across multiple languages that doesn't lead to insane amounts of boilerplate... some reasons:
Show this thread
2
2
And then here's me exploring what I now realize is a step towards reinventing path-dependent types:
Quote Tweet
Mathematica experiment showing how I wish generics in type systems worked.
Show this thread
2
4
Ooh, this is quite interesting. I also like the `Unique[..]` thing. I've been thinking of separating out nominalness from data type definitions in a similar way in my experiments. 🤔
1
Also worth looking at the section titled “Nominality through ascription” in the above linked paper.
2
1
Seems like te path-dependent types of DOT let you avoid having a source of uniqueness and still support equality & subtyping constraints, as well as nominal types. I need to play with it a bit myself.
1
1
Interesting! Yeah, I wasn't aware they did. I'm going to be using dependent-records-as-modules in my language, and was interested how I could get nominality in. I was only really aware of how ML does it, and the stuff talked about in the _1ML with Special Effects_ paper…