{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Multicurryable (
Multicurryable (..),
NP (..),
NS (..),
I (..),
) where
import Data.Kind
import Data.SOP
type Multicurryable :: (Type -> Type -> Type) -> [Type] -> Type -> Type -> Constraint
class
Multicurryable (f :: Type -> Type -> Type) (items :: [Type]) a curried
| f items a -> curried,
f curried -> items a
where
type UncurriedArgs f :: [Type] -> Type
multiuncurry :: curried -> f (UncurriedArgs f items) a
multicurry :: f (UncurriedArgs f items) a -> curried
type family IsFunction f :: Bool where
IsFunction (_ -> _) = 'True
IsFunction _ = 'False
instance
MulticurryableF (IsFunction curried) items a curried =>
Multicurryable (->) items a curried
where
type UncurriedArgs (->) = NP I
multiuncurry :: curried -> UncurriedArgs (->) items -> a
multiuncurry = forall (b :: Bool) (items :: [*]) a curried.
MulticurryableF b items a curried =>
curried -> NP I items -> a
multiuncurryF @(IsFunction curried)
multicurry :: (UncurriedArgs (->) items -> a) -> curried
multicurry = forall (b :: Bool) (items :: [*]) a curried.
MulticurryableF b items a curried =>
(NP I items -> a) -> curried
multicurryF @(IsFunction curried)
class
MulticurryableF (b :: Bool) items a curried
| items a -> curried,
b curried -> items a
where
multiuncurryF :: curried -> NP I items -> a
multicurryF :: (NP I items -> a) -> curried
instance MulticurryableF 'False '[] a a where
multiuncurryF :: a -> NP I '[] -> a
multiuncurryF a
a NP I '[]
Nil = a
a
multicurryF :: (NP I '[] -> a) -> a
multicurryF NP I '[] -> a
f = NP I '[] -> a
f forall {k} (a :: k -> *). NP a '[]
Nil
instance
MulticurryableF (IsFunction curried) rest tip curried =>
MulticurryableF 'True (i ': rest) tip (i -> curried)
where
multiuncurryF :: (i -> curried) -> NP I (i : rest) -> tip
multiuncurryF i -> curried
f (I x
x :* NP I xs
rest) =
forall (b :: Bool) (items :: [*]) a curried.
MulticurryableF b items a curried =>
curried -> NP I items -> a
multiuncurryF @(IsFunction curried) @rest @tip @curried (i -> curried
f x
x) NP I xs
rest
multicurryF :: (NP I (i : rest) -> tip) -> i -> curried
multicurryF NP I (i : rest) -> tip
f i
i =
forall (b :: Bool) (items :: [*]) a curried.
MulticurryableF b items a curried =>
(NP I items -> a) -> curried
multicurryF @(IsFunction curried) @rest @tip @curried forall a b. (a -> b) -> a -> b
$ \NP I rest
rest -> NP I (i : rest) -> tip
f (forall a. a -> I a
I i
i forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I rest
rest)
type family IsEither f :: Bool where
IsEither (Either _ _) = 'True
IsEither _ = 'False
instance
MulticurryableE (IsEither curried) items a curried =>
Multicurryable Either items a curried
where
type UncurriedArgs Either = NS I
multiuncurry :: curried -> Either (UncurriedArgs Either items) a
multiuncurry = forall (b :: Bool) (items :: [*]) a curried.
MulticurryableE b items a curried =>
curried -> Either (NS I items) a
multiuncurryE @(IsEither curried)
multicurry :: Either (UncurriedArgs Either items) a -> curried
multicurry = forall (b :: Bool) (items :: [*]) a curried.
MulticurryableE b items a curried =>
Either (NS I items) a -> curried
multicurryE @(IsEither curried)
class
MulticurryableE (b :: Bool) items a curried
| items a -> curried,
b curried -> items a
where
multiuncurryE :: curried -> Either (NS I items) a
multicurryE :: Either (NS I items) a -> curried
instance MulticurryableE 'False '[] a a where
multiuncurryE :: a -> Either (NS I '[]) a
multiuncurryE = forall a b. b -> Either a b
Right
multicurryE :: Either (NS I '[]) a -> a
multicurryE = \case
Left NS I '[]
impossible -> case NS I '[]
impossible of {}
Right a
a -> a
a
instance
MulticurryableE (IsEither curried) rest tip curried =>
MulticurryableE 'True (i ': rest) tip (Either i curried)
where
multiuncurryE :: Either i curried -> Either (NS I (i : rest)) tip
multiuncurryE = \case
Left i
x -> forall a b. a -> Either a b
Left (forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (forall a. a -> I a
I i
x))
Right curried
rest ->
case forall (b :: Bool) (items :: [*]) a curried.
MulticurryableE b items a curried =>
curried -> Either (NS I items) a
multiuncurryE @(IsEither curried) @rest @tip @curried curried
rest of
Left NS I rest
ns -> forall a b. a -> Either a b
Left (forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S NS I rest
ns)
Right tip
x -> forall a b. b -> Either a b
Right tip
x
multicurryE :: Either (NS I (i : rest)) tip -> Either i curried
multicurryE = \case
Left NS I (i : rest)
rest -> case NS I (i : rest)
rest of
Z (I x
x) -> forall a b. a -> Either a b
Left x
x
S NS I xs
rest' -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (b :: Bool) (items :: [*]) a curried.
MulticurryableE b items a curried =>
Either (NS I items) a -> curried
multicurryE @(IsEither curried) @_ @tip @curried (forall a b. a -> Either a b
Left NS I xs
rest')
Right tip
tip -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (b :: Bool) (items :: [*]) a curried.
MulticurryableE b items a curried =>
Either (NS I items) a -> curried
multicurryE @(IsEither curried) @_ @tip @curried (forall a b. b -> Either a b
Right tip
tip)