首页 文章

构造具有简单求和类型的所有值的n元产品

提问于
浏览
2

我正在使用generics-sop库 . 我想写一个具有以下类型的值:

values :: forall r. IsEnumType r => NP (K r) (Code r)

也就是说,对于构造函数没有任何参数(IsEnumType)的sum类型,我想生成一个n-ary乘积(NP),其中contains是每个点的相应构造函数值 .

例如,对于类型

{-# LANGUAGE DeriveGeneric #-}

import qualified GHC.Generics as GHC
import Generics.SOP

data Foo = Bar
         | Baz
         deriving (GHC.Generic)

instance Generic Foo

我想 生产环境 n-ary产品

K Bar :* K Baz :* Nil

我相信解决方案将涉及转换带有每个构造函数的通用表示的n-ary产品,所以我写了这个:

values :: forall r. IsEnumType r => NP (K r) (Code r)
values = liftA_NP (mapKK (to . SOP))  _

使用liftA_NPmapKK . 但我不确定如何自己生成通用表示 .

2 回答

  • 1

    您可以使用现有的 injectionsapInjs* 函数 .

    apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs
    

    你必须提供函数参数的产品,在我们的通用情况下,每个组件将应用于基础数据类型的一个构造函数 .

    但是因为我们假设一个枚举类型,所以这些构造函数都没有任何参数,我们可以在任何地方提供空的参数列表!

    values :: forall r . IsEnumType r => NP (K r) (Code r)
    values =
      map_NP
        (mapKK (to . SOP))
        (apInjs'_NP
          (cpure_NP (Proxy @((~) '[])) Nil)
        )
    
  • 1

    也许有一种更简单的方法,但我设法通过使用辅助类型类 POSN 定义 values ,它基本上对空类型级列表的类型级列表执行归纳:

    values :: forall r c. (Generic r, Code r ~ c, POSN c) => NP (K r) c
    values = liftA_NP (mapKK (to . SOP)) posn
    
    -- products of sums of nil
    class POSN xss where
        posn :: NP (K (NS (NP I) xss)) xss   
    
    instance POSN '[] where
        posn = Nil
    
    instance (SListI2 xss, POSN xss) => POSN ('[] ': xss) where
        posn = let previous = posn @xss
                in K (Z Nil) :* liftA_NP (mapKK S) previous
    

    内部 NP 总是 Nil ,因为它们对应于每个构造函数的参数,并且从不存在任何参数 .

    归纳步骤为列表的其余部分的每个总和“加1”,在头部预先设置为“零” .

    使用示例:

    ghci> :set -XTypeApplications
    ghci> values @Foo
    K Bar :* K Baz :* Nil
    

相关问题