Type-level sets in GHC

#1

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?

2 Likes
#2

…otherwise:

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

#3

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.

#4

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.

#5

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
#6

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.

#7

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?

#8
#9

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