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?

3 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!

2 Likes
#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
1 Like
#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
#10

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?

2 Likes
#11

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

3 Likes
#12

Oh that’s interesting!!

#13

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

#14

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.