{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Multicurryable (
Multicurryable (..),
MulticurryableF,
IsFunction,
MulticurryableE,
IsEither,
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 IsFunction :: Type -> Where
type family IsFunction f :: Where where
IsFunction (_ -> _) = 'NotYetThere
IsFunction _ = 'AtTheTip
instance
MulticurryableF items a curried (IsFunction curried)
=>
Multicurryable (->) items a curried
where
type UncurriedArgs (->) = NP I
multiuncurry :: curried -> UncurriedArgs (->) items -> a
multiuncurry = forall (items :: [*]) a curried (decomp :: Where).
MulticurryableF items a curried decomp =>
curried -> NP I items -> a
multiuncurryF @_ @_ @_ @(IsFunction curried)
multicurry :: (UncurriedArgs (->) items -> a) -> curried
multicurry = forall (items :: [*]) a curried (decomp :: Where).
MulticurryableF items a curried decomp =>
(NP I items -> a) -> curried
multicurryF @_ @_ @_ @(IsFunction curried)
type MulticurryableF :: [Type] -> Type -> Type -> Where -> Constraint
class
MulticurryableF items a curried (decomp :: Where)
| items a -> curried decomp,
curried decomp -> items a
where
multiuncurryF :: curried -> NP I items -> a
multicurryF :: (NP I items -> a) -> curried
instance MulticurryableF '[] a a 'AtTheTip 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 rest tip curried (IsFunction curried)
=>
MulticurryableF (i ': rest) tip (i -> curried) 'NotYetThere
where
multiuncurryF :: (i -> curried) -> NP I (i : rest) -> tip
multiuncurryF i -> curried
f (I x
x :* NP I xs
rest) =
forall (items :: [*]) a curried (decomp :: Where).
MulticurryableF items a curried decomp =>
curried -> NP I items -> a
multiuncurryF @rest @tip @curried @(IsFunction 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 (items :: [*]) a curried (decomp :: Where).
MulticurryableF items a curried decomp =>
(NP I items -> a) -> curried
multicurryF @rest @tip @curried @(IsFunction 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 IsEither :: Type -> Where
type family IsEither f :: Where where
IsEither (Either _ _) = 'NotYetThere
IsEither _ = 'AtTheTip
instance
MulticurryableE items a curried (IsEither curried) =>
Multicurryable Either items a curried
where
type UncurriedArgs Either = NS I
multiuncurry :: curried -> Either (UncurriedArgs Either items) a
multiuncurry = forall (items :: [*]) a curried (decomp :: Where).
MulticurryableE items a curried decomp =>
curried -> Either (NS I items) a
multiuncurryE @_ @_ @_ @(IsEither curried)
multicurry :: Either (UncurriedArgs Either items) a -> curried
multicurry = forall (items :: [*]) a curried (decomp :: Where).
MulticurryableE items a curried decomp =>
Either (NS I items) a -> curried
multicurryE @_ @_ @_ @(IsEither curried)
type MulticurryableE :: [Type] -> Type -> Type -> Where -> Constraint
class
MulticurryableE items a curried (decomp :: Where)
| items a -> curried decomp,
curried decomp -> items a
where
multiuncurryE :: curried -> Either (NS I items) a
multicurryE :: Either (NS I items) a -> curried
instance MulticurryableE '[] a a 'AtTheTip 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 rest tip curried (IsEither curried) =>
MulticurryableE (i ': rest) tip (Either i curried) 'NotYetThere
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 (items :: [*]) a curried (decomp :: Where).
MulticurryableE items a curried decomp =>
curried -> Either (NS I items) a
multiuncurryE @rest @tip @curried @(IsEither 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 (items :: [*]) a curried (decomp :: Where).
MulticurryableE items a curried decomp =>
Either (NS I items) a -> curried
multicurryE @_ @tip @curried @(IsEither 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 (items :: [*]) a curried (decomp :: Where).
MulticurryableE items a curried decomp =>
Either (NS I items) a -> curried
multicurryE @_ @tip @curried @(IsEither curried) (forall a b. b -> Either a b
Right tip
tip)
data Where =
NotYetThere
| AtTheTip