Is it possible to declare FromJSON instance for my weird enum-like type?

Question

I'm trying to define a type that can be restricted to a subset of Nat's. While I realise a simple solution would be to use a regular ADT I'm still curious if such type could be defined with an accompanying FromJSON instance. 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

This can be then used as follows:

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

I was able to define a ToJSON instance:

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

However it doesn't seem declaring a FromJSON instance is possible as I can't figure out how to convince the compiler that whatever number I might get out of a JSON document is indeed a member of the set of accepted values of SomeEnum.

My question then is - is it possible to declare that instance at all with the current formulation of the data type? Could perhaps the type itself be adjusted somehow to allow for such instance while preserving the behaviour of being restricted to specific set of Nats?

I'm not very familiar with Haskell's type level features so perhaps what I'm asking doesn't make sense in its current form. I would appreciate any comments.

It should be possible, but it will be awkward and require that the FromJSON instance reflect xs down to the value level in order to verify that the parsed number is an element of xs. Doing that will require being able to express that every element of xs has a KnownNat constraint, which can be done, but will be... awkward. — Carl
This might be impossible because you are trying to make a value with a type that depends on what is in the JSON. In theory, using an existential to say that it is some number rather than any specific number should sidestep the issue, but I think you will still have to provide a witness, which would require dependent types. — Lazersmoke
@Lazersmoke SomeEnum is the existential needed. And GHC.TypeLits has the necessary machinery to create a witness at runtime, suitable for stuffing into the existential. — Carl
@Lazersmoke is thinking along the right lines. It's not impossible but it won't be pretty, especially not with the TypeLits/Proxy setup you have at the moment. You'll need to use a singleton to prove that the n fits the bound and then existentially quantify it. I will note that your SomeEnum is basically Fin, modulo some sort of mapping from the Fin values to the Nats in your type level list — Benjamin Hodgson
Oh, I missed the problem.. The other constraint needs a witness, too. Ok, allowing a runtime witness for that constraint is possible, but it will involve an unsafeCoerce. So.. Maybe not worth it. You'd have to implement very carefully to preserve type safety. — Carl

rampion rampion · Accepted Answer · 2017-05-24T19:19:08

It's easier to look at your problem without the distraction of JSON.

The real problem is can you define a function

toSomeEnum :: Integer -> SomeEnum xs

Since SomeEnum [] is isomorphic to Void, and -1 is not convertable to SomeEnum xs for any xs, obviously not. We need the ability to fail:

toSomeEnum :: Integer -> Maybe (SomeEnum xs)

And to do anything beyond const Nothing we'll need the ability to compare the elements of xs to the 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]

This 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]

Which can be fixed by using a lazier definition of Or:

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

No unsafeCoerce or type witnesses required. Your calling code simply has to know what it expects xs to be.

λ 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"

Is it possible to declare FromJSON instance for my weird enum-like type?

1 Answers