Haskell/Agdaのタイプレベルセット

Question

最新版のGHCでは、タイプレベルのリストがサポートされています。しかし、私はアプリケーションの型レベルセットを扱う必要があり、型レベルのリストに基づいて型レベルのセットライブラリを実装したいと考えています。しかし、私はHaskellでタイプレベルのセットをサポートしている任意のライブラリがあります:(

を開始する場所を知らない

が

Answer 1

あなたはHListパッケージからHList年代のためHSetプロパティを使用することができます？

{-# 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のインスタンスを書く必要があります。