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!


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?

1 Like

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 :smiley: 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.

I think we needs several ingredients:

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?


@jvanbruegge is working on type-level sets and maps! For first-class records and effect systems.


Oh that’s interesting!!

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.