代码之家  ›  专栏  ›  技术社区  ›  dbanas

在haskell中,如何使用类型的派生泛型实例,从有限离散类型的值转换为(有限n)并返回?

representable deriving enumerable generics haskell
  •  1
  • dbanas  · 技术社区  · 8 年前

    我有一个库,它当前要求用户提供类型为的helper函数: 

    tEnum :: (KnownNat n) => MyType -> Finite n

    以便库实现可以使用类型为的函数的非常有效的大小向量表示: 

    foo :: MyType -> a

    ( MyType 是离散和有限的。)

    假设 Generic 实例 MyType 有可能,有没有办法产生 tEnum 自动地,从而减轻我的图书馆用户的负担?

    我还想走另一条路,也就是说,自动导出: 

    tGen :: (KnownNat n) => Finite n -> MyType
    1 回复  |  直到 8 年前
        1
  •  1
  •   Lucy Maya Menon    8 年前

    我有些东西至少在 tEnum 事情的另一面。因为您没有指定 Finite 我用我自己的 有限的 和 Nat .

    我在文章的底部提供了一个完整的代码片段和一个示例,但只讨论一般编程部分,而不涉及peano算术的合理标准构造和各种有用的定理。

    typeClass用于跟踪可以转换为/不转换为这些有限枚举的内容。这里重要的一点是默认类型签名和默认定义:这意味着如果有人派生 EnumFin 为了一个班级 Generic ,它们不必实际编写任何代码,因为将使用这些默认值。默认值使用另一个类的方法,该类是为 GHC.Generics 可以生产。注意,普通签名和默认签名都使用 (n ~ ...) => ... n 而不是写 有限的 直接在类型签名中;这是因为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

    类中实际上还有一些其他实用方法。这些由实际的泛型实现使用,以获得最小/最大值。 Finite n 由实现产生( 0 和 n )不必使用更多的类型类&传播 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)

    泛型类的类声明相当简单;但是请注意,它的参数是kind * -> * ,不是 * 以下内容: 

    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 是一个非常简单的构造函数,指的是一个没有字段的构造函数,它只是被编码为 有限的 数 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)

    对于单个构造函数字段,还有一个重要的实例,它要求包含的类型也实现 枚举 以下内容: 

    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

    为了完整起见,这里有一个完整的文件,它定义了 纳特 / 有限的 上面使用的基础设施和使用 通用的 实施: 

    {-# 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
    推荐文章
    关于   移动版
    代码之家 - 一站式码农服务社区
    沪ICP备11025650号