Haskell: At least one maybe field

AtLeastOneMaybe.md

Suppose we have:

data MyType  = MyType
  { myTypeA :: Maybe A 
  , myTypeB :: Maybe B
  }

How do we guarantee that at least one field is non empty?

type AtLeastOne :: Maybe a -> Maybe b -> Bool
type family AtLeastOne f1 f2 where
  AtLeastOne ('Just _) _ = 'True
  AtLeastOne _ ('Just _) = 'True
  AtLeastOne _ _ = 'False

type Maybe2 :: Maybe a -> Maybe b -> Type
data Maybe2 f1 f2 where
  MkMaybe2 ::
    (AtLeastOne f1 f2 ~ 'True) =>
    Sing f1 ->
    Sing f2 ->
    Maybe2 f1 f2

maybe2_ok = MkMaybe2 (SJust STrue) SNothing
maybe2_ok' = MkMaybe2 (SJust STrue) (SJust STrue)
-- BOGUS
-- maybe2_ko = MkMaybe2 SNothing SNothing

Then, to make this equivalent, you need to existentialize it:

type Sigma2 :: forall s1 -> forall s2 -> (s1 ~> (s2 ~> Type)) -> Type
data Sigma2 (s1 :: Type) (s2 :: Type) :: (s1 ~> s2 ~> Type) -> Type where
  (:&&:) ::
    forall s1 s2 t fst snd.
    Sing (fst :: s1) ->
    Sing (snd :: s2) ->
    (t @@ fst) @@ snd ->
    Sigma2 s1 s2 t
infixr 4 :&&:

type SomeMaybe2 = forall a b. Sigma (Maybe a) (Maybe b) (TyCon2 Maybe2)

Can we generalize the above?

type AtLeastOne :: [Maybe a] -> Bool
type family AtLeastOne xs where
  AtLeastOne '[] = 'False
  AtLeastOne ('Just _ ': _) = 'True
  AtLeastOne (_ ': xs) = AtLeastOne xs

type MaybeN :: [Maybe Bool] -> Type
data MaybeN xs where
  MaybeN ::
    (AtLeastOne xs ~ 'True) =>
    Sing xs  ->
    MaybeN xs

type SomeMaybeN = Sigma [Maybe Bool] (TyCon1 MaybeN)

maybeN_ok = MaybeN $ SCons (SJust STrue) (SCons SNothing SNil)
maybeN_ok' = MaybeN $ SCons (SJust STrue) (SCons (SJust STrue) SNil)
-- BOGUS
-- maybeN_ko = MaybeN $ SCons SNothing (SCons SNothing SNil)

maybeN_ok_some :: SomeMaybeN
maybeN_ok_some = xs :&: MaybeN xs where
  xs = SCons (SJust STrue) (SCons SNothing SNil)

The only problem here is that I couldn't write type MaybeN :: [forall a. Maybe a] -> Type. Maybe, it's possible to do that, but I couldn't find a way. A workaround is to define a union type like in 'Data types à la carte'.

A better solution from @FlyingGuibou

data Maybe2 bool a where
  Nothing2 :: Maybe2 'False a
  Just2 :: a -> Maybe2 'True a

type family Or' a :: Constraint where
  Or' ('True : xs) = ()
  Or' (_ : xs) = Or' xs

data A

data B

data MyType where
  MyType ::
    Or' '[a, b] =>
    { myTypeA :: Maybe2 a A,
      myTypeB :: Maybe2 b B
    } ->
    MyType

Another solution from @gallais:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind

data IMaybe (b :: Bool) (a :: Type) where
  IJust :: a -> IMaybe True a
  INothing :: IMaybe False a

type family (||) (b :: Bool) (c :: Bool) :: Bool where
  True || c = True
  False || c = c

data A = A
data B = B
data C = C

data MyType = forall a b c. (a || b || c) ~ True => MyType
  { myTypeA :: IMaybe a A
  , myTypeB :: IMaybe b B
  , myTypeC :: IMaybe c C
  }

myValC :: MyType
myValC = MyType INothing INothing (IJust C)

myValAC :: MyType
myValAC = MyType (IJust A) INothing (IJust C)

fail :: MyType
fail = MyType INothing INothing INothing