{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
module Symantic.Syntaxes.CurryN where
import Data.Function (($), (.))
import Data.Kind (Type)
import Symantic.Syntaxes.EithersOfTuples (Tuples)
class CurryN args where
curryN :: (Tuples args -> res) -> args -..-> res
uncurryN :: (args -..-> res) -> Tuples args -> res
mapresultN :: (a -> b) -> (args -..-> a) -> args -..-> b
instance CurryN '[a] where
curryN :: forall res. (Tuples '[a] -> res) -> '[a] -..-> res
curryN = (Tuples '[a] -> res) -> '[a] -..-> res
forall a b. (a -> b) -> a -> b
($)
uncurryN :: forall res. ('[a] -..-> res) -> Tuples '[a] -> res
uncurryN = ('[a] -..-> res) -> Tuples '[a] -> res
forall a b. (a -> b) -> a -> b
($)
mapresultN :: forall a b. (a -> b) -> ('[a] -..-> a) -> '[a] -..-> b
mapresultN = (a -> b) -> ('[a] -..-> a) -> '[a] -..-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
instance CurryN (b ': as) => CurryN (a ': b ': as) where
curryN :: forall res. (Tuples (a : b : as) -> res) -> (a : b : as) -..-> res
curryN Tuples (a : b : as) -> res
f a
x = forall (args :: [*]) res.
CurryN args =>
(Tuples args -> res) -> args -..-> res
curryN @(b ': as) (\Tuples (b : as)
xs -> Tuples (a : b : as) -> res
f (a
x, Tuples (b : as)
xs))
uncurryN :: forall res. ((a : b : as) -..-> res) -> Tuples (a : b : as) -> res
uncurryN (a : b : as) -..-> res
f (a
x, Tuples (b : as)
xs) = forall (args :: [*]) res.
CurryN args =>
(args -..-> res) -> Tuples args -> res
uncurryN @(b ': as) ((a : b : as) -..-> res
a -> b -> as -..-> res
f a
x) Tuples (b : as)
xs
mapresultN :: forall a b.
(a -> b) -> ((a : b : as) -..-> a) -> (a : b : as) -..-> b
mapresultN a -> b
f (a : b : as) -..-> a
as2r = forall (args :: [*]) a b.
CurryN args =>
(a -> b) -> (args -..-> a) -> args -..-> b
mapresultN @(b ': as) a -> b
f ((b -> as -..-> a) -> b -> as -..-> b)
-> (a -> b -> as -..-> a) -> a -> b -> as -..-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a : b : as) -..-> a
a -> b -> as -..-> a
as2r
type family (args :: [Type]) -..-> (r :: Type) :: Type where
'[] -..-> r = r
(a : args) -..-> r = a -> args -..-> r
type family Args (f :: Type) :: [Type] where
Args (a -> r) = a : Args r
Args r = '[]
type family Result (as :: Type) :: Type where
Result (a -> r) = Result r
Result r = r