{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE UndecidableInstances #-} -- | Tuples-of-Functions module Symantic.Syntaxes.TuplesOfFunctions where import Data.Bool (Bool (..)) import Data.Either (Either (..)) import Data.Function qualified as Fun import Data.Kind (Type) -- * Type 'ToF' type ToF a next = ToFIf (IsToF a) a next -- ** Type 'ToFIf' -- | Transform a type @(a)@ to Tuples-of-Functions returning @(next)@. -- The @(t)@ parameter is to avoid overlapping instances of 'UnToFIf'. type family ToFIf t a next :: Type where -- For '<.>': curry. ToFIf 'True (a, b) next = ToF a (ToF b next) -- For '<+>', request both branches. ToFIf 'True (Either l r) next = (ToF l next, ToF r next) -- Useless to ask '()' as argument. ToFIf 'True () next = next -- Everything else becomes a new argument. ToFIf 'False a next = a -> next -- ** Type 'IsToF' -- | This 'Bool' is added to 'ToFIf' to avoid overlapping instances. type family IsToF a :: Bool where IsToF () = 'True IsToF (a, b) = 'True IsToF (Either l r) = 'True IsToF a = 'False -- * Type 'UnToF' type UnToF a = UnToFIf (IsToF a) a -- * Class 'UnToFIf' class UnToFIf (t :: Bool) a where unToF :: ToFIf t a next -> a -> next instance UnToFIf 'True () where unToF = Fun.const instance (UnToF a, UnToF b) => UnToFIf 'True (a, b) where unToF hab (a, b) = (unToF @(IsToF b) (unToF @(IsToF a) hab a)) b instance (UnToF a, UnToF b) => UnToFIf 'True (Either a b) where unToF (ha, hb) = \case Left a -> unToF @(IsToF a) ha a Right b -> unToF @(IsToF b) hb b instance UnToFIf 'False a where unToF = Fun.id