如何解决在类型系列中匹配无效的 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 举报,一经查实,本站将立刻删除。