Can I declare a FromJSON instance for my weird enum type?
I am trying to define a type that can be limited to a subset Nat
. While I understand that a simple solution would be to use a regular ADT, I am still wondering if such a type could be defined with an accompanying instance FromJSON
. Here's what I have so far:
{-# 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
Then it can be used like this:
λ> SomeEnum (Proxy :: Proxy 1) :: SomeEnum [1,2]
I managed to define an instance ToJSON
:
instance ToJSON (SomeEnum xs) where toJSON (SomeEnum n) = Number (fromIntegral . natVal $ n)
However, this does not mean that an instance FromJSON
is possible, as I cannot figure out how to convince the compiler that any number I could get from the JSON document is indeed a member of the set of accepted values SomeEnum
.
My question then is, is it possible at all to declare this instance as the current data type formulation? Perhaps the type itself can be somehow adjusted to provide such an instance while still retaining the behavior limited to a specific set of Nat
s?
I'm not very familiar with Haskell-level functions, so maybe what I'm asking doesn't make sense in its current form. Any comments would be appreciated.
source to share
It's easier to look at your problem without JSON distraction.
The real problem is that you can define a function
toSomeEnum :: Integer -> SomeEnum xs
Since it SomeEnum []
is isomorphic Void
and -1
cannot be converted to
SomeEnum xs
for any xs
, obviously not. We need an error:
toSomeEnum :: Integer -> Maybe (SomeEnum xs)
To do anything outside const Nothing
, we'll need the ability to compare elements xs
for runtime input:
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]
It didn't quite work as GHC complained
• 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]
What can be fixed by using a lazier definition Or
:
type family Or (a :: Bool) (b :: Bool) :: Bool where
Or 'True _ = 'True
Or _ 'True = 'True
Or _ _ = 'False
No unsafeCoerce
or bring in witnesses. Your calling code just needs to know what it is expecting 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"
source to share