closer.hs

{-# Language RankNTypes, TypeInType, ConstraintKinds, GADTs, TypeFamilies, TypeOperators, DataKinds #-}
module Tree where

import Data.Kind
import Data.Bifunctor

data SomeN (f :: k) where
  Base :: f -> SomeN f
  Step :: (forall a. SomeN (f a)) -> SomeN f

data T (f :: k -> Constraint) (g :: k) = V (SomeN g)


example1 :: (forall a. f a) -> T Functor f
example1 fa = V (Step (Base fa))

example1' :: T Functor f -> f a
example1' (V (Step (Base fa))) = fa

example2 :: (forall a b. f a b) -> T Bifunctor f
example2 fab = V (Step (Step (Base fab)))

example2' :: T Bifunctor f -> f a b
example2' (V (Step (Step (Base fab)))) = fab

currying.hs

{-# Language GADTs, TypeFamilies, TypeOperators, DataKinds #-}
module Tree where

import GHC.TypeLits

data Args :: [*] -> * where
  Nil  ::                 Args '[]
  (:-) :: a -> Args as -> Args (a ': as)

infixr 5 :-

class Curry xs where
  type Curried xs r
  curryN :: (Args xs -> r) -> Curried xs r

instance Curry '[] where
  type Curried '[] r = r
  curryN f = f Nil

instance Curry as => Curry (a ': as) where
  type Curried (a ': as) r = a -> Curried as r
  curryN f x = curryN (\xs -> f (x :- xs))

tuple3 :: Args '[a,b,c] -> (a,b,c)
tuple3 (x :- y :- z :- Nil) = (x,y,z)

tuple3_curried :: a -> b -> c -> (a,b,c)
tuple3_curried = curryN tuple3

usinganewtype.hs

{-# Language RankNTypes, TypeInType, ConstraintKinds, GADTs, TypeFamilies, TypeOperators, DataKinds #-}
module Tree where

import Data.Kind
import Data.Bifunctor

data family AllN (f :: k)
newtype instance AllN a = Base a
newtype instance AllN f = Step (forall a. AllN (f a))

newtype T (f :: k -> Constraint) (g :: k) = V (AllN g)


example1 :: (forall a. f a) -> T Functor f
example1 fa = V (Step (Base fa))

example1' :: T Functor f -> f a
example1' (V (Step (Base fa))) = fa

example2 :: (forall a b. f a b) -> T Bifunctor f
example2 fab = V (Step (Step (Base fab)))

example2' :: T Bifunctor f -> f a b
example2' (V (Step (Step (Base fab)))) = fab