Type-Level-Sets in Haskell/Agda

Question

Ich habe gesehen, dass es in den neuesten Versionen von GHC Unterstützung für Typenlisten gibt. Allerdings muss ich mit Typ-Level-Sets für eine Anwendung arbeiten und möchte eine Set-Level-Set-Bibliothek basierend auf Typ-Level-Listen implementieren. Aber ich weiß nicht, wo :(

zu starten Gibt es eine Bibliothek unterstützt Typ-Level-Sets in Haskell

Answer 1

Sie HSet Eigenschaft für HList ‚s aus HList Paket verwenden kann:?

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

für die Arbeit mit anderen Typen müssen Sie HEq Instanzen für sie schreiben ..