Type-level sets in Haskell / Agda

dependent-type, haskell

Solution

You can use HSet property for HList's from HList package:

{-# LANGUAGE FlexibleInstances #-}

import Data.HList

class (HList l, HSet l) => ThisIsSet l where
  -- Here we have @l@ which is @HList@ _and_ @HSet@.
  test :: l

-- This is ok:

instance ThisIsSet HNil where
  test = hNil

-- And this:

instance ThisIsSet (HCons HZero HNil) where
  test = hCons hZero hNil

-- And this (HZero != HSucc HZero):

instance ThisIsSet (HCons HZero (HCons (HSucc HZero) HNil)) where
  test = hCons hZero (hCons (hSucc hZero) hNil)

-- This is an error since HSucc HZero == HSucc HZero:

instance ThisIsSet (HCons (HSucc HZero) (HCons (HSucc HZero) HNil)) where
  test = hCons (hSucc hZero) (hCons (hSucc hZero) hNil)

for working with other types you need to write HEq instances for them.

Problem

I've seen that in the latest versions of GHC there's support for type-level lists. However, I need to work with type-level sets for an application, and would like to implement a type-level set library based on type-level lists. But I don't know where to start :( Is there any library supporting type-level sets in Haskell?

Original source