我有一个库，目前要求用户提供一个类型为的助手函数
tEnum :: (KnownNat n) => MyType -> Finite n
以便库实现可以使用类型为的函数的非常有效的大小矢量表示
foo :: MyType -> a
(MyType是离散的和有限的。(
假设为MyType派生一个Generic实例是可能的，那么有没有一种方法可以自动生成tEnum，从而减轻我的库用户的负担？
我也想走另一条路；即自动导出：
tGen :: (KnownNat n) => Finite n -> MyType
我至少在tEnum方面有一些工作。由于您没有指定Finite的代表，我使用了我自己的Finite和Nat。
我在文章的底部包含了一个完整的代码片段和一个例子，但只讨论通用编程部分，忽略了Peano算术的合理标准构造和各种有用的定理
类型类用于跟踪可以转换为这些有限枚举的内容。这里重要的一点是默认类型签名和默认定义：这意味着，如果有人为派生Generic的类派生EnumFin，他们实际上不必编写任何代码，因为将使用这些默认值。默认值使用另一个类中的方法，该类是为GHC.Generics可以生成的各种东西实现的。注意，正常签名和默认签名都使用(n ~ ...) => ... n，而不是直接在类型签名中写入Finite的大小；这是因为GHC将检测到默认签名不必与常规签名匹配(在定义Size但不定义fromFin或toFin的类实现的情况下(：
class EnumFin a where
type Size a :: Nat
type Size a = GSize (Rep a)
toFin :: (n ~ Size a) => a -> Finite n
default toFin :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> a -> Finite n
toFin = gToFin . from
fromFin :: (n ~ Size a) => Finite n -> a
default fromFin :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> Finite n -> a
fromFin = to . gFromFin
实际上，该类中还有一些其他实用程序方法。这些由实际的通用实现来获得由实现(0和n(产生的最小/最大CCD_；传播KnownNat样式约束：
zero :: (n ~ Size a) => Finite n
default zero :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> Finite n
zero = gzero @(Rep a)
gt :: (n ~ Size a) => Finite n
default gt :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> Finite n
gt = ggt @(Rep a)
泛型类的类声明相当简单；但是请注意，它的参数是* -> *，而不是*:
class GEnumFin f where
type GSize f :: Nat
gToFin :: f a -> Finite (GSize f)
gFromFin :: Finite (GSize f) -> f a
gzero :: Finite (GSize f)
ggt :: Finite (GSize f)
这个泛型类现在必须为每个相关的泛型构造函数实现。例如，U1是一个非常简单的构造函数，指的是一个没有字段的构造函数，它只是被编码为Finite数字0:
instance GEnumFin U1 where
type GSize U1 = 'Z
gToFin U1 = ZF ZS
gFromFin (ZF ZS) = U1
gzero = ZF ZS
ggt = ZF ZS
:*:用于组合各个字段，因此两个部分都需要编码(它编码lhs*(m+1)+rhs，其中m是rhs的最大值(：
instance forall a b. (GEnumFin a, GEnumFin b) => GEnumFin (a :*: b) where
type GSize (a :*: b) = Plus (Times (GSize a) ('S (GSize b))) (GSize b)
gToFin (a :*: b) = addFin (mulFin (gToFin a) (SF (ggt @b))) (gToFin b)
gFromFin x = (gFromFin a :*: gFromFin b)
where (a, b) = quotRemFin (toSN (ggt @a)) (toSN (ggt @b)) x
gzero = addFin (mulFin (gzero @a) (SF (ggt @b))) (gzero @b)
ggt = addFin (mulFin (ggt @a) (SF (ggt @b))) (ggt @b)
另一方面，:+:在表示和时使用，因此必须能够对其任何组成部分进行编码(它将左手边编码为0..n，将右手边编码为n+1...n+1+m(：
instance forall a b. (GEnumFin a, GEnumFin b) => GEnumFin (a :+: b) where
type GSize (a :+: b) = 'S (Plus (GSize a) (GSize b))
gToFin (L1 a) = case proofPlusComm (toSN (gzero @a)) (toSN (gzero @b)) of
Refl -> addFin (injFin (gzero @b)) (gToFin a)
gToFin (R1 b) = addFin (SF (ggt @a)) (gToFin b)
gFromFin x = case proofPlusComm (toSN (ggt @a)) (toSN (ggt @b)) of
Refl -> splitFin (toSN (ggt @b)) (toSN (ggt @a)) x
(R1 . gFromFin @b) (L1 . gFromFin @a)
gzero = addFin (injFin (gzero @a)) (gzero @b)
ggt = addFin (SF (ggt @a)) (ggt @b)
单个构造函数字段还有一个重要的实例，它要求包含的类型也实现EnumFin:
instance (EnumFin a) => GEnumFin (K1 i a) where
type GSize (K1 i a) = Size a
gToFin (K1 a) = toFin a
gFromFin = K1 . fromFin
gzero = zero @a
ggt = gt @a
最后，有必要实现M1构造函数，它用于将元数据附加到通用树，而我们在这里根本不关心它：
instance forall i c a. (GEnumFin a) => GEnumFin (M1 i c a) where
type GSize (M1 i c a) = GSize a
gToFin (M1 a) = gToFin a
gFromFin = M1 . gFromFin
gzero = gzero @a
ggt = ggt @a
为了完整起见，这里有一个完整的文件，定义了上面使用的所有Nat/Finite基础设施，并展示了使用Generic实现：
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveGeneric #-}
import GHC.Generics
import Data.Type.Equality
-- Fairly standard Peano naturals & various useful theorems about them:
data Nat = Z | S Nat
data SNat (n :: Nat) where
ZS :: SNat 'Z
SS :: SNat n -> SNat ('S n)
deriving instance Show (SNat n)
type family Plus (n :: Nat) (m :: Nat) where
Plus 'Z m = m
Plus ('S n) m = 'S (Plus n m)
plus :: SNat n -> SNat m -> SNat (Plus n m)
plus ZS m = m
plus (SS n) m = SS (plus n m)
proofPlusNZ :: SNat n -> Plus n 'Z :~: n
proofPlusNZ ZS = Refl
proofPlusNZ (SS n) = case proofPlusNZ n of Refl -> Refl
proofPlusNS :: SNat n -> SNat m -> Plus n ('S m) :~: 'S (Plus n m)
proofPlusNS ZS _ = Refl
proofPlusNS (SS n) m = case proofPlusNS n m of Refl -> Refl
proofPlusAssoc :: SNat n -> SNat m -> SNat o
-> Plus n (Plus m o) :~: Plus (Plus n m) o
proofPlusAssoc ZS _ _ = Refl
proofPlusAssoc (SS n) ZS _ = case proofPlusNZ n of Refl -> Refl
proofPlusAssoc (SS n) (SS m) ZS =
case proofPlusNZ m of
Refl -> case proofPlusNZ (plus n (SS m)) of
Refl -> Refl
proofPlusAssoc (SS n) (SS m) (SS o) =
case proofPlusAssoc n (SS m) (SS o) of Refl -> Refl
proofPlusComm :: SNat n -> SNat m -> Plus n m :~: Plus m n
proofPlusComm ZS ZS = Refl
proofPlusComm ZS (SS m) = case proofPlusNZ m of Refl -> Refl
proofPlusComm (SS n) ZS = case proofPlusNZ n of Refl -> Refl
proofPlusComm (SS n) (SS m) =
case proofPlusComm (SS n) m of
Refl -> case proofPlusComm n (SS m) of
Refl -> case proofPlusComm n m of
Refl -> Refl
type family Times (n :: Nat) (m :: Nat) where
Times 'Z m = 'Z
Times ('S n) m = Plus m (Times n m)
times :: SNat n -> SNat m -> SNat (Times n m)
times ZS _ = ZS
times (SS n) m = plus m (times n m)
proofMultNZ :: SNat n -> Times n 'Z :~: 'Z
proofMultNZ ZS = Refl
proofMultNZ (SS n) = case proofMultNZ n of Refl -> Refl
proofMultNS :: SNat n -> SNat m -> Times n ('S m) :~: Plus n (Times n m)
proofMultNS ZS ZS = Refl
proofMultNS ZS (SS m) =
case proofMultNZ (SS m) of
Refl -> case proofMultNZ m of
Refl -> Refl
proofMultNS (SS n) ZS =
case proofMultNS n ZS of Refl -> Refl
proofMultNS (SS n) (SS m) =
case proofMultNS (SS n) m of
Refl -> case proofMultNS n (SS m) of
Refl -> case proofMultNS n m of
Refl -> case lemma1 n m (times n (SS m)) of
Refl -> Refl
where lemma1 :: SNat n -> SNat m -> SNat o -> Plus n ('S (Plus m o))
:~:
'S (Plus m (Plus n o))
lemma1 n' m' o' =
case proofPlusComm n' (SS (plus m' o')) of
Refl -> case proofPlusComm m' (plus n' o') of
Refl -> case proofPlusAssoc m' o' n' of
Refl -> case proofPlusComm n' o' of
Refl -> Refl
proofMultSN :: SNat n -> SNat m -> Times ('S n) m :~: Plus (Times n m) m
proofMultSN ZS m = case proofPlusNZ m of Refl -> Refl
proofMultSN (SS n) m =
case proofPlusNZ (times n m) of
Refl -> case proofPlusComm m (plus m (plus (times n m) ZS)) of
Refl -> Refl
proofMultComm :: SNat n -> SNat m -> Times n m :~: Times m n
proofMultComm ZS ZS = Refl
proofMultComm ZS (SS m) = case proofMultNZ (SS m) of
Refl -> case proofMultComm ZS m of
Refl -> Refl
proofMultComm (SS n) ZS = case proofMultComm n ZS of Refl -> Refl
proofMultComm (SS n) (SS m) =
case proofMultNS n m of
Refl -> case proofMultNS m n of
Refl -> case proofPlusAssoc m n (times n m) of
Refl -> case proofPlusAssoc n m (times m n) of
Refl -> case proofPlusComm n m of
Refl -> case proofMultComm n m of
Refl -> Refl
-- `Finite n` represents a number in 0..n (inclusive).
--
-- Notice that the "zero" branch includes an `SNat`; this is useful to be
-- able to conveniently write `toSN` below (generally, to be able to
-- reflect the `n` component to the value level) without needing to use a
-- singleton typeclass & pass constraitns around everywhere.
--
-- It should be possible to switch this out for other implementations of
-- `Finite` with different choices, but may require rewriting many of
-- the following functions.
data Finite (n :: Nat) where
ZF :: SNat n -> Finite n
SF :: Finite n -> Finite ('S n)
deriving instance Show (Finite n)
toSN :: Finite n -> SNat n
toSN (ZF sn) = sn
toSN (SF f) = SS (toSN f)
addFin :: forall n m. Finite n -> Finite m -> Finite (Plus n m)
addFin (ZF n) (ZF m) = ZF (plus n m)
addFin (ZF n) (SF b) =
case proofPlusNS n (toSN b) of
Refl -> SF (addFin (ZF n) b)
addFin (SF a) b = SF (addFin a b)
mulFin :: forall n m. Finite n -> Finite m -> Finite (Times n m)
mulFin (ZF n) (ZF m) = ZF (times n m)
mulFin (ZF n) (SF b) = case proofMultNS n (toSN b) of
Refl -> addFin (ZF n) (mulFin (ZF n) b)
mulFin (SF a) b = addFin b (mulFin a b)
quotRemFin :: SNat n -> SNat m -> Finite (Plus (Times n ('S m)) m)
-> (Finite n, Finite m)
quotRemFin nn mm xx = go mm xx nn mm (ZF ZS) (ZF ZS)
where go :: forall n m s p q r.
( Plus q s ~ n, Plus r p ~ m)
=> SNat m
-> Finite (Plus (Times s ('S m)) p)
-> SNat s
-> SNat p
-> Finite q
-> Finite r
-> (Finite n, Finite m)
go _ (ZF _) s p q r = (addFin q (ZF s), addFin r (ZF p))
go m (SF x) s (SS p) q r =
case proofPlusComm (SS p) (times s m) of
Refl -> case proofPlusNS (times s (SS m)) p of
Refl -> case proofPlusNS (toSN r) p of
Refl -> go m x s p q (SF r)
go m (SF x) (SS s) ZS q _ =
case proofPlusNS (toSN q) s of
Refl -> case proofMultSN s (SS m) of
Refl -> case proofPlusNS (times s (SS m)) m of
Refl -> case proofPlusComm (times s (SS m)) (SS m) of
Refl -> case proofPlusNZ (times (SS s) (SS m)) of
Refl -> go m x s m (SF q) (ZF ZS)
splitFin :: forall n m a. SNat n -> SNat m -> Finite ('S (Plus n m))
-> (Finite n -> a) -> (Finite m -> a) -> a
splitFin nn mm xx f g = go nn mm xx mm (ZF ZS)
where go :: forall r s. (Plus r s ~ m)
=> SNat n -> SNat m -> Finite ('S (Plus n s))
-> SNat s -> Finite r -> a
go _ _ (ZF _) s r = g (addFin r (ZF s))
go n m (SF x) (SS s) r =
case proofPlusNS (toSN r) s of
Refl -> case proofPlusNS n s of
Refl -> go n m x s (SF r)
go n _ (SF x) ZS _ = case proofPlusNZ n of Refl -> f x
injFin :: Finite n -> Finite ('S n)
injFin (ZF n) = ZF (SS n)
injFin (SF a) = SF (injFin a)
toNum :: (Num a) => Finite n -> a
toNum (ZF _) = 0
toNum (SF n) = 1 + toNum n
-- The actual classes & Generic stuff:
class EnumFin a where
type Size a :: Nat
type Size a = GSize (Rep a)
toFin :: (n ~ Size a) => a -> Finite n
default toFin :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> a -> Finite n
toFin = gToFin . from
fromFin :: (n ~ Size a) => Finite n -> a
default fromFin :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> Finite n -> a
fromFin = to . gFromFin
zero :: (n ~ Size a) => Finite n
default zero :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> Finite n
zero = gzero @(Rep a)
gt :: (n ~ Size a) => Finite n
default gt :: (Generic a, GEnumFin (Rep a), n ~ GSize (Rep a))
=> Finite n
gt = ggt @(Rep a)
class GEnumFin f where
type GSize f :: Nat
gToFin :: f a -> Finite (GSize f)
gFromFin :: Finite (GSize f) -> f a
gzero :: Finite (GSize f)
ggt :: Finite (GSize f)
instance GEnumFin U1 where
type GSize U1 = 'Z
gToFin U1 = ZF ZS
gFromFin (ZF ZS) = U1
gzero = ZF ZS
ggt = ZF ZS
instance forall a b. (GEnumFin a, GEnumFin b) => GEnumFin (a :*: b) where
type GSize (a :*: b) = Plus (Times (GSize a) ('S (GSize b))) (GSize b)
gToFin (a :*: b) = addFin (mulFin (gToFin a) (SF (ggt @b))) (gToFin b)
gFromFin x = (gFromFin a :*: gFromFin b)
where (a, b) = quotRemFin (toSN (ggt @a)) (toSN (ggt @b)) x
gzero = addFin (mulFin (gzero @a) (SF (ggt @b))) (gzero @b)
ggt = addFin (mulFin (ggt @a) (SF (ggt @b))) (ggt @b)
instance forall a b. (GEnumFin a, GEnumFin b) => GEnumFin (a :+: b) where
type GSize (a :+: b) = 'S (Plus (GSize a) (GSize b))
gToFin (L1 a) = case proofPlusComm (toSN (gzero @a)) (toSN (gzero @b)) of
Refl -> addFin (injFin (gzero @b)) (gToFin a)
gToFin (R1 b) = addFin (SF (ggt @a)) (gToFin b)
gFromFin x = case proofPlusComm (toSN (ggt @a)) (toSN (ggt @b)) of
Refl -> splitFin (toSN (ggt @b)) (toSN (ggt @a)) x
(R1 . gFromFin @b) (L1 . gFromFin @a)
gzero = addFin (injFin (gzero @a)) (gzero @b)
ggt = addFin (SF (ggt @a)) (ggt @b)
instance forall i c a. (GEnumFin a) => GEnumFin (M1 i c a) where
type GSize (M1 i c a) = GSize a
gToFin (M1 a) = gToFin a
gFromFin = M1 . gFromFin
gzero = gzero @a
ggt = ggt @a
instance (EnumFin a) => GEnumFin (K1 i a) where
type GSize (K1 i a) = Size a
gToFin (K1 a) = toFin a
gFromFin = K1 . fromFin
gzero = zero @a
ggt = gt @a
-- Demo:
data Foo = A | B deriving (Show, Generic)
data Bar = C | D deriving (Show, Generic)
data Baz = E Foo | F Bar | G Foo Bar deriving (Show, Generic)
instance EnumFin Foo
instance EnumFin Bar
instance EnumFin Baz
main :: IO ()
main = do
putStrLn $ show $ toNum @Integer $ gt @Baz
putStrLn $ show $ toNum @Integer $ toFin $ E A
putStrLn $ show $ toNum @Integer $ toFin $ E B
putStrLn $ show $ toNum @Integer $ toFin $ F C
putStrLn $ show $ toNum @Integer $ toFin $ F D
putStrLn $ show $ toNum @Integer $ toFin $ G A C
putStrLn $ show $ toNum @Integer $ toFin $ G A D
putStrLn $ show $ toNum @Integer $ toFin $ G B C
putStrLn $ show $ toNum @Integer $ toFin $ G B D
putStrLn $ show $ fromFin @Baz $ toFin $ E A
putStrLn $ show $ fromFin @Baz $ toFin $ E B
putStrLn $ show $ fromFin @Baz $ toFin $ F C
putStrLn $ show $ fromFin @Baz $ toFin $ F D
putStrLn $ show $ fromFin @Baz $ toFin $ G A C
putStrLn $ show $ fromFin @Baz $ toFin $ G A D
putStrLn $ show $ fromFin @Baz $ toFin $ G B C
putStrLn $ show $ fromFin @Baz $ toFin $ G B D