Type-level sets in GHC

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?



Making heterogenous sets from heterogenous lists is left as an exercise…

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-Nothing Maybe.

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.

Lists can be fine, but you’ll need functions that normalise them.

An example of such a type level API is here (using liftE for normalization):

Not sure it’s worth it.

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!

1 Like

Actually I was suggested the exact same yesterday :slight_smile:
Yes if there are 2 points of variations, then 2 tags could be appropriate. You just have to pray that this never changes.

Cool, I did not know about type data.

I know:

— Worked on type level sets some time ago. Perhaps they can comment on the state of the art so far?

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”.