Как перейти от значения конечного дискретного типа к (конечному n) и обратно, используя производный экземпляр типа Generic, в Haskell?

Question

Как перейти от значения конечного дискретного типа к (конечному n) и обратно, используя производный экземпляр типа Generic, в Haskell?

У меня есть библиотека, которая в настоящее время требует от пользователей, чтобы они предоставили вспомогательную функцию с типом:

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

так что реализация библиотеки может использовать очень эффективное размерное векторное представление функции с типом:

foo :: MyType -> a

(MyType является дискретным и конечным.)

Предполагая, что вывод Generic экземпляр для MyType возможно, есть ли способ генерировать tEnum автоматически, таким образом снимая это бремя с пользователей моей библиотеки?

Я также хотел бы пойти другим путем; то есть автоматически выводим:

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

1

haskell generics enumerable deriving representable

Источник

user1549736 14 июл '18 в 02:10

1 ответ

Решение

Другие вопросы по тегам haskell generics enumerable deriving representable

user6676199 14 июл '18 в 09:35 2018-07-14 09:35 · Accepted Answer · 2018-07-14 09:35

У меня есть кое-что, по крайней мере tEnum сторона вещей. Поскольку вы не указали свое представление Finite Я использовал свой собственный Finite а также Nat,

Я включил полный фрагмент кода с примером в конце поста, но буду обсуждать только общие части программирования, оставляя в стороне достаточно стандартную конструкцию арифметики Пеано и различные полезные теоремы об этом.

Класс типов используется для отслеживания вещей, которые могут быть преобразованы в / из этих конечных перечислений. Важный бит здесь - это сигнатуры типов по умолчанию и определения по умолчанию: это означает, что если кто-то выведет EnumFin для получения класса Genericим не нужно писать какой-либо код, так как эти значения по умолчанию будут использоваться. По умолчанию используются методы из другого класса, который реализован для различных видов вещей, которые 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

На самом деле в классе есть также несколько других служебных методов. Они используются фактической универсальной реализацией, чтобы получить минимум / максимум 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)

Объявление класса для универсального класса довольно просто; обратите внимание, однако, что его параметр является добрым * -> *не *:

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