Haskell/Agda中的類型集合

我已經看到，在最新版本的GHC中，支持類型級別列表。但是，我需要爲應用程序使用類型級別的集合，並且希望基於類型級別的列表實現類型級別的集合庫。但我不知道從哪裏開始:(Haskell/Agda中的類型集合

是否有任何支持的類型級套在Haskell庫

2013-08-26 serras

那麼各種可擴展的記錄庫給你set-ish操作（union，檢查標籤是否在記錄中），甚至如果實現不是像Data.Set那樣的樹。查看列表，或該頁面上的其他位。 – aavogt

現在有[圖書館]（https://hackage.haskell.org/package/type-level-sets）提供這個。 –

可以使用HSet屬性HList的從HList包：

{-# LANGUAGE FlexibleInstances #-} 

import Data.HList 

class (HList l, HSet l) => ThisIsSet l where 
    -- Here we have @[email protected] which is @[email protected] _and_ @[email protected] 
    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

來源

2013-08-29 05:26:12 JJJ

Haskell/Agda中的類型集合

回答

相關問題