{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}

module Type.Data.Bool
    ( C(switch)
    , Singleton(False, True)
    , singleton
    , True
    , true
    , False
    , false
    , Not
    , not
    , (:&&:)
    , and
    , (:||:)
    , or
    , If
    , if_
    ) where

import Type.Base.Proxy (Proxy(Proxy))
import Data.Typeable (Typeable)

import qualified Prelude


class C bool where switch :: f False -> f True -> f bool
instance C False where switch :: f False -> f True -> f False
switch f False
f f True
_ = f False
f
instance C True where switch :: f False -> f True -> f True
switch f False
_ f True
f = f True
f

data Singleton bool where
    False :: Singleton False
    True :: Singleton True

singleton :: (C bool) => Singleton bool
singleton :: Singleton bool
singleton = Singleton False -> Singleton True -> Singleton bool
forall bool (f :: * -> *). C bool => f False -> f True -> f bool
switch Singleton False
False Singleton True
True

data True deriving (Typeable)
true :: Proxy True
true :: Proxy True
true = Proxy True
forall a. Proxy a
Proxy
instance Prelude.Show True where
    show :: True -> String
show True
_ = String
"True"
data False deriving (Typeable)
false :: Proxy False
false :: Proxy False
false = Proxy False
forall a. Proxy a
Proxy
instance Prelude.Show False where
    show :: False -> String
show False
_ = String
"False"

type family Not x
type instance Not False = True
type instance Not True  = False
not :: Proxy x -> Proxy (Not x)
not :: Proxy x -> Proxy (Not x)
not Proxy x
Proxy = Proxy (Not x)
forall a. Proxy a
Proxy

type family x :&&: y
type instance False :&&: _x = False
type instance True  :&&: x = x
and :: Proxy x -> Proxy y -> Proxy (x :&&: y)
and :: Proxy x -> Proxy y -> Proxy (x :&&: y)
and Proxy x
Proxy Proxy y
Proxy = Proxy (x :&&: y)
forall a. Proxy a
Proxy

type family x :||: y
type instance True  :||: _x = True
type instance False :||: x = x
or :: Proxy x -> Proxy y -> Proxy (x :||: y)
or :: Proxy x -> Proxy y -> Proxy (x :||: y)
or Proxy x
Proxy Proxy y
Proxy = Proxy (x :||: y)
forall a. Proxy a
Proxy

type family If x y z
type instance If True y _z = y
type instance If False _y z = z
if_ :: Proxy x -> Proxy y -> Proxy z -> Proxy (If x y z)
if_ :: Proxy x -> Proxy y -> Proxy z -> Proxy (If x y z)
if_ Proxy x
Proxy Proxy y
Proxy Proxy z
Proxy = Proxy (If x y z)
forall a. Proxy a
Proxy