Вопросы Теги

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

Я считаю, что @Matthew Crumley прав. Они функционально , если не структурно, эквивалентны. Если вы используете Firebug для просмотра объектов, созданных с помощью new, вы можете видеть, что они одинаковы. Однако, мое предпочтение было бы следующим. Я предполагаю, что это просто похоже на то, к чему я привык в C # / Java. То есть, определите класс, определите поля, конструктор и методы. 

var A = function() {};
A.prototype = {
    _instance_var: 0,

    initialize: function(v) { this._instance_var = v; },

    x: function() {  alert(this._instance_var); }
};

EDIT Не означает, что область действия переменной была закрытой, я просто пытался показать, как я определите мои классы в javascript. Имя переменной было изменено, чтобы отразить это.

1
задан dbanas 14 July 2018 в 02:10
поделиться

1 ответ

У меня есть что-то, работающее, по крайней мере, на стороне 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) без необходимости использования большего количества типов типов и amp; распространять 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)

Этот класс generics теперь должен быть реализован для каждого из соответствующих генерических конструкторов. Например, 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
1
ответ дан Peter Amidon 17 August 2018 в 12:02
поделиться
  • 1
    Благодаря! Есть ли причина, по которой вы решили определить свой собственный Finite, а не использовать Data.Finite? Кроме того, важно ли правильное функционирование вашего кода, чтобы диапазон Finite n был [0, n], а не [0, n), как используется в Data.Finite? – dbanas 14 July 2018 в 15:16
  • 2
    Казалось, что вокруг было несколько различных конечных реализаций, и я не был уверен, какой из них вы используете, поэтому было проще всего быстро написать его. Не следует слишком тяжело переводить идею на Data.Finite, но вам может понадобиться использовать небезопасные операции, реализующие quotRemFin и splitFin. Ряд Finite сделал несколько доказательств более легко, но не должен быть ужасно важным; Я думаю, что основные отличия состоят в том, что GSize (a :*: b) должен быть a*m+b вместо a*(m+1)+b, а GSize (a :+: b) должен быть a+b вместо a+b+1. – Peter Amidon 14 July 2018 в 15:46
Другие вопросы по тегам:

Похожие вопросы: