haskell - 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インスタンスを記述する必要があります。