haskell - 是否可以为我奇怪的类似枚举类型声明 FromJSON 实例？

Question

我正在尝试定义一个可以限制为 Nat 子集的类型。虽然我意识到一个简单的解决方案是使用常规 ADT，但我仍然很好奇是否可以使用随附的 FromJSON 实例来定义此类类型。这是我到目前为止所拥有的:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Test where

import Control.Monad
import Data.Aeson
import Data.Kind (Constraint)
import Data.Proxy
import Data.Type.Equality
import GHC.TypeLits
import Prelude


type family Or (a :: Bool) (b :: Bool) :: Bool where
  Or 'False 'False = 'False
  Or 'True 'False = 'True
  Or 'False 'True = 'True
  Or 'True 'True = 'True

type family IsOneOf (n :: Nat) (xs :: [Nat]) :: Bool where
  IsOneOf n '[] = 'False
  IsOneOf n (x ': xs) = Or (n == x) (IsOneOf n xs)

type family Member n xs :: Constraint where
  Member n xs = 'True ~ IsOneOf n xs

data SomeEnum (xs :: [Nat]) where
        SomeEnum :: (KnownNat n, Member n xs) => Proxy n -> SomeEnum xs

然后可以按如下方式使用:

λ> SomeEnum (Proxy :: Proxy 1) :: SomeEnum [1,2]

我能够定义一个 ToJSON 实例:

instance ToJSON (SomeEnum xs) where
  toJSON (SomeEnum n) = Number (fromIntegral . natVal $ n)

但是，声明 FromJSON 实例似乎是不可能的，因为我不知道如何说服编译器，无论我从 JSON 文档中得到的数字确实是SomeEnum 可接受的值集。

我的问题是 - 是否可以使用数据类型的当前表述来声明该实例？也许可以以某种方式调整类型本身以允许这种情况，同时保留仅限于特定 Nat 集合的行为？

我不太熟悉 Haskell 的类型级别功能，所以也许我所问的内容在当前形式下没有意义。如果有任何意见，我将不胜感激。

Answer 1

不受 JSON 干扰，可以更轻松地查看问题。

真正的问题是你能定义一个函数吗

toSomeEnum :: Integer -> SomeEnum xs

由于 SomeEnum [] 与 Void 同构，并且 -1 不可转换为SomeEnum xs 对于任何 xs 来说，显然不是。我们需要有失败的能力:

toSomeEnum :: Integer -> Maybe (SomeEnum xs)

要执行 const Nothing 之外的任何操作，我们需要能够比较将 xs 元素添加到运行时输入:

toSomeEnum' :: forall xs. ToSomeEnum xs => Integer -> Maybe (SomeEnum xs)
toSomeEnum' n = do
  SomeNat proxy_n <- someNatVal n
  toSomeEnum proxy_n

class ToSomeEnum (xs :: [Nat]) where
  toSomeEnum :: forall (n :: Nat). KnownNat n => Proxy n -> Maybe (SomeEnum xs)

instance ToSomeEnum '[] where
  toSomeEnum = const Nothing

instance (KnownNat x, ToSomeEnum xs) => ToSomeEnum (x ': xs) where
  toSomeEnum proxy_n = case sameNat proxy_n (Proxy @x) of 
    Just Refl -> Just (SomeEnum proxy_n) -- [1]
    Nothing -> case toSomeEnum proxy_n :: Maybe (SomeEnum xs) of
      Nothing -> Nothing
      Just (SomeEnum proxy_n') -> Just (SomeEnum proxy_n') -- [2]

正如 GHC 提示的那样，这不太有效

• Could not deduce: Or 'True (IsOneOf n xs) ~ 'True
    arising from a use of ‘SomeEnum’
  from the context: x ~ n
    bound by a pattern with constructor:
               Refl :: forall k (a :: k). a :~: a,
             in a case alternative
    at [1]
...
• Could not deduce: Or (GHC.TypeLits.EqNat n1 x) 'True ~ 'True
    arising from a use of ‘SomeEnum’
  from the context: (KnownNat n1, Member n1 xs)
    bound by a pattern with constructor:
               SomeEnum :: forall (xs :: [Nat]) (n :: Nat).
                           (KnownNat n, Member n xs) =>
                           Proxy n -> SomeEnum xs,
             in a case alternative
    at [2]

这可以通过使用 Or 的惰性定义来修复:

type family Or (a :: Bool) (b :: Bool) :: Bool where
  Or 'True _ = 'True
  Or _ 'True = 'True
  Or _ _ = 'False

不需要 unsafeCoerce 或类型见证。您的调用代码只需知道它期望 xs 是什么。

λ case (toSomeEnum' 1 :: Maybe (SomeEnum '[1,2,3])) of { Just _ -> "ok" ; Nothing -> "nope" }
"ok"
λ case (toSomeEnum' 4 :: Maybe (SomeEnum '[1,2,3])) of { Just _ -> "ok" ; Nothing -> "nope" }
"nope"