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

Question

我在使用涉及 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)

标签： haskelltype-level-computation