是否有可能爲我的奇怪枚舉類型聲明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] 

可固定使用LAZ IER的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"