Type Sets in Haskell / Agda

Question

I have seen that in recent versions of GHC there is support for type lists. However, I need to work with typeset typesets for the application and would like to implement a type set library based on type lists. But I do not know where to start :(

Is there a library that supports level type sets in Haskell?

Answer 1

You can use the HSet property for the HList 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) 

to work with other types you need to write HEq for them.