在类型系列中匹配无效的 Nat 表达式，例如 (0 - 1)

问题描述

我在处理涉及 Nat 类型的表达式时遇到困难，我需要 ConstructorByPosition 为无效位置返回 'nothing，但通配符匹配失败。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE polyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test where

import GHC.Generics
import GHC.TypeLits
import GHC.Types

-- | How to match on "invalid" Nat type such as (0 - 1)?
--
-- λ> :set -XDataKinds
-- λ> :kind! ConstructorByPosition 1 (Maybe Char)
-- ConstructorByPosition 2 (Maybe Char) :: Maybe Symbol
-- = 'Just "Just"
-- λ> :kind! ConstructorByPosition 5 (Maybe Char)
-- ConstructorByPosition 5 (Maybe Char) :: Maybe Symbol
-- = 'nothing
--
-- Hoping for 'nothing,but...
--
-- λ> :kind! ConstructorByPosition 0 (Maybe Char)
-- ConstructorByPosition 0 (Maybe Char) :: Maybe Symbol
-- = GConstructorByPosition (0 - 1)
--      (M1 C ('MetaCons "Just" 'PrefixI 'False)
--            (S1 ('MetaSel 'nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Char)))

type family ConstructorByPosition (cpos :: Nat) (a :: *) :: Maybe Symbol where
  ConstructorByPosition cpos a = GConstructorByPosition cpos (Rep a)

type family GConstructorByPosition (cpos :: Nat) (f :: * -> *) :: Maybe Symbol where
  GConstructorByPosition cpos (D1 m f) = GConstructorByPosition cpos f
  GConstructorByPosition cpos (f :+: g) =
    Alt (GConstructorByPosition cpos f)
        (GConstructorByPosition (cpos - GConstructorCount f) g)
  GConstructorByPosition 1 (C1 ('MetaCons cname _ _) _) = 'Just cname
  GConstructorByPosition _ _ = 'nothing

type family Alt (m1 :: Maybe a) (m2 :: Maybe a) :: Maybe a where
  Alt ('Just a) _ = 'Just a
  Alt _ b = b

type family GConstructorCount (r :: k -> Type) :: Nat where
  GConstructorCount (D1 c f) = GConstructorCount f
  GConstructorCount (f :+: g)  = GConstructorCount f + GConstructorCount g
  GConstructorCount (C1 c f) = 1
  GConstructorCount f = TypeError ('ShowType f)

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）