Since DataKinds (and recently TypeData) I find myself toying more and more with taggging data types with various properties instead of producing variants. One such example is FFI Ptr. I’d love to have Pointer [ReadOnly, NonNull] a, but native lists don’t work very well because Pointer [ReadOnly, ReadOnly, ReadOnly] a is utterly useless.
In practice this could translate to APIs looking like:
peek :: forall (s :: [Property]) (a :: Type) . Ptr s a -> IO a
poke :: forall (s :: [Property]) (a :: Type) .
(ReadWrite ∈ s)
=> Ptr s a
-> a
-> IO ()
So, I wonder what it would take to implement type-level sets. Perhaps I’m thinking too much about it and something like s :: Set [Property] could work, perhaps with type errors in case of duplication?
How are you going enforce the ReadOnly or the NonNull? You can ask for (ReadOnly ∈ s) =>, but
what you really want is (ReadWrite /∈ s) =>;
or equivalently that a Property list cannot contain both ReadOnly and ReadWrite – which is the same difficulty as ruling out umpty repeats of ReadOnly [**];
whatever happens inside the IO () is ‘on its honour’ to keep within the claimed properties.
So this is no sort of type guarantee, just at best machine-checked documentation.
[**] The HList 2003 paper that @atravers links to has some examples, using overlapping instances and ‘impossible’ constraints (or TypeFamilies in later versions). It’s messy and the authors weren’t even convinced themselves.
NonNull is a property of a pointer value, not its type. Asking for a NonNull value is same as asking for a non-NothingMaybe.
The usual way to enforce properties like this is to put the sensitive functions inside a package but not export them; the public interface provides meaningfully-named and run-time checked aliases.
For something explicitly with two-levels like this, I tend to actually prefer polymorphism. This works when you’ve got some operaions that work in any state, and some that only work in a more limited state:
peek :: Ptr rw a -> IO a
poke :: Ptr 'Write a -> a -> IO a
Now peek works in any state, but the moment you poke something you force rw ~ 'Write. This doesn’t really answer your general question, but maybe this will be useful!
Actually I was suggested the exact same yesterday
Yes if there are 2 points of variations, then 2 tags could be appropriate. You just have to pray that this never changes.
red-black-record was my attempt at avoiding the “sorted list of fields” approach, by using an actual type-level red-black-tree. Symbols are the only supported keys/elements because I don’t know how to “compare” two arbitrary types (IIRC, isovector’s library uses a compiler plugin for that).
In the end, the experiment wasn’t very successful because:
Compile times are still bad.
When you “show” a type-level map, it spits out the internals of the red-black-tree, which is pretty unreadable compared to a list representation. I don’t know how to hide the internals of type-level data structures.
I didn’t know how to convince GHC of basic facts like “if you take out an element from the set, and then add it back, you end up with the same set”.
type level sets is something I really, really would like to have because it’s sometimes my first thought but then immediately followed by “ugh, but they’re not available”. I just created an account just for this reply I have some thoughts, but they are super amateurish because I really have no experience with interacting with GHC.
I don’t think the “type level lists as sets” is the way to go. Not ergonomic.
I think they are doable as a compiler plugin, I would prefer not use type-families because they are so slow, but one can always improve later. There is already a first idea here on how to compare types, it’s on GitHub from isovector (type-sets is the repo called)
While I personally have never ever interacted with GHC, I am really quite interested in this and so have a rough idea how to do it, although it might be impossible because of details unknown to me. And some things I am not sure about.
representation: I don’t actually know, but maybe a type-level red-black-tree or an underlying list
transformation and reasoning: maybe start with type-families and see how much one can do? They tend to slow down GHC and consume ungodly amounts of memory. GHC plugins can give GHC some reasoning capabilities. I think maybe basic reasoning is enough for most use-cases?
One major question I am really unsure about is the syntax-sugar, which I think is essential. It’s just too unergonomic otherwise. You can just provide a “to data structure” type-level function if you’re really interested what’s currently behind the sugar.
I think parsing sytanx sugar is doable with the approach mentioned, but will it always display it this way? I think every basic function acting on the syntax-sugar would need to be implemented as a GHC-Plugin because we want to “hide” the under the HsExpansion mentioned here in the wiki above? Or is there some other way?
I would be really interested whether my approach is realistic. I completely expect it to be a lot of work and just lack any real experience for this. But in principle this would lead to a first-class type-set like thing…right?
I don’t think type level sets are useful for effect libraries. You sometimes end up with more than one effect E on the stack and that’s fine, e.g. if you are in E :> es0 => Eff es0, you use runE :: Eff (E : es) a -> Eff es a to be in E :> es0 => Eff (E : es0), then you abstract away to get E :> es => Eff es which makes you “forget” about the E :> es0 constraint, but it’s still there and can be used (by other effects in scope for example).
I had a post about unordered effects and it uses an ergonomic list interface to type-level sets. The catch is that removing an element from such a type-level set seems very hard, if doable at all. There are probably other operations that don’t translate well.