Skip to content

Instantly share code, notes, and snippets.

@kosmikus
Created October 20, 2018 06:32
Show Gist options
  • Save kosmikus/482be398be4397d6a8742347f02c9c2a to your computer and use it in GitHub Desktop.
Save kosmikus/482be398be4397d6a8742347f02c9c2a to your computer and use it in GitHub Desktop.
Curry / uncurry in generics-sop
{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableSuperClasses, TypeApplications #-}
{-# LANGUAGE ConstraintKinds #-}
module CurryNP4 where
import Data.Kind
import Generics.SOP
import GHC.Exts
curryNP :: forall xs a f r . (C a f xs r) => a -> (NP f xs -> r)
curryNP k =
case sList :: SList xs of
SNil -> \ Nil -> k
SCons -> \ (x :* xs) -> curryNP (k x) xs
uncurryNP :: forall xs a f r . C a f xs r => (NP f xs -> r) -> a
uncurryNP k =
case sList :: SList xs of
SNil -> k Nil
SCons -> \ x -> uncurryNP (\ xs -> k (x :* xs))
curryNPI :: forall xs a r . CI a xs r => a -> (NP I xs -> r)
curryNPI k =
case sList :: SList xs of
SNil -> \ Nil -> k
SCons -> \ (I x :* xs) -> curryNPI (k x) xs
uncurryNPI :: forall xs a r . CI a xs r => (NP I xs -> r) -> a
uncurryNPI k =
case sList :: SList xs of
SNil -> k Nil
SCons -> \ x -> uncurryNPI (\ xs -> k (I x :* xs))
type C a f xs r = (Curry a f xs r, Uncurry a f xs r, SListI xs)
type CI a xs r = (CurryI a xs r, UncurryI a xs r, SListI xs)
type family Uncurry (a :: Type) (f :: k -> Type) (xs :: [k]) (r :: Type) :: Constraint where
Uncurry a f '[] r = (r ~ a)
Uncurry a f (x : xs) r = (a ~ (Arg a -> Res a), Arg a ~ f x, Uncurry (Res a) f xs r)
type family Curry (a :: Type) (f :: k -> Type) (xs :: [k]) (r :: Type) :: Constraint where
Curry (g x -> a) f xs r = (f ~ g, xs ~ (Head xs : Tail xs), Head xs ~ x, Curry a f (Tail xs) r)
Curry a f xs r = (r ~ a, xs ~ '[])
type family UncurryI (a :: Type) (xs :: [k]) (r :: Type) :: Constraint where
UncurryI a '[] r = (r ~ a)
UncurryI a (x : xs) r = (a ~ (Arg a -> Res a), Arg a ~ x, UncurryI (Res a) xs r)
type family CurryI (a :: Type) (xs :: [k]) (r :: Type) :: Constraint where
CurryI (x -> a) xs r = (xs ~ (Head xs : Tail xs), Head xs ~ x, CurryI a (Tail xs) r)
CurryI a xs r = (r ~ a, xs ~ '[])
type family Arg (x :: Type) :: Type where
Arg (a -> r) = a
type family Res (x :: Type) :: Type where
Res (a -> r) = r
type family Head (xs :: [k]) :: k where
Head (x : xs) = x
type family Tail (xs :: [k]) :: [k] where
Tail (x : xs) = xs
test3 :: String
test3 = uncurryNP showNP (I True) (I 5) (I 'x')
test3I :: String
test3I = uncurryNPI showNP True 'x' 5
test3' = uncurryNP showNP'
test3I' = uncurryNPI showNP'
showNP :: All Show xs => NP I xs -> String
showNP = concat . hcollapse . hcmap (Proxy @Show) (mapIK show)
showNP' :: NP I '[Int, Char, Bool] -> String
showNP' = showNP
test4 = curryNP (\ (I x) (I y) (I z) -> (x + y + z :: Int))
test4I = curryNPI (\ x y z -> x + y + z :: Int)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment