Haskell / Agda中的类型级集合

Question

我看到最新版本的GHC支持类型级别列表。然而，我的应用需要处理类型级别集合，并且我想基于类型级别列表实现一个类型级别集合库。但是我不知道从哪里开始 :(

是否有支持Haskell中类型级别集合的库？

- serras

---

各种可扩展记录库提供了类似集合的操作（并集、检查标签是否在记录中），即使实现不像Data.Set那样是一棵树。请查看列表http://www.haskell.org/haskellwiki/Extensible_record#Libraries_on_hackage或该页面上的其他内容。 - aavogt

现在有一个库提供了这个功能。链接 - Will Sewell

Answer 1

您可以使用HSet属性来自HList包的HList：

{-# 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)

与其他类型一起使用，您需要为它们编写HEq实例。

- JJJ