{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeOperators        #-}

-- We need undecidable instances for the definition of @Foldr@,
-- and @Domains@ and @CoDomain@ using @If@ for instance.
{-# LANGUAGE UndecidableInstances #-}

module Agda.Utils.TypeLevel where

import Data.Kind ( Type )
import Data.Proxy
import GHC.Exts (Constraint)

------------------------------------------------------------------
-- CONSTRAINTS
------------------------------------------------------------------

-- | @All p as@ ensures that the constraint @p@ is satisfied by
--   all the 'types' in @as@.
--   (Types is between scare-quotes here because the code is
--   actually kind polymorphic)

type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where
  All p '[]       = ()
  All p (a ': as) = (p a, All p as)

------------------------------------------------------------------
-- FUNCTIONS
-- Type-level and Kind polymorphic versions of usual value-level
-- functions.
------------------------------------------------------------------

-- | On Booleans
type family If (b :: Bool) (l :: k) (r :: k) :: k where
  If 'True  l r = l
  If 'False l r = r

-- | On Lists
type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where
  Foldr c n '[]       = n
  Foldr c n (a ': as) = c a (Foldr c n as)

-- | Version of @Foldr@ taking a defunctionalised argument so
--   that we can use partially applied functions.
type family Foldr' (c :: Function k (Function l l -> Type) -> Type)
                   (n :: l) (as :: [k]) :: l where
  Foldr' c n '[]       = n
  Foldr' c n (a ': as) = Apply (Apply c a) (Foldr' c n as)

type family Map (f :: Function k l -> Type) (as :: [k]) :: [l] where
  Map f as = Foldr' (ConsMap0 f) '[] as

data ConsMap0 :: (Function k l -> Type) -> Function k (Function [l] [l] -> Type) -> Type
data ConsMap1 :: (Function k l -> Type) -> k -> Function [l] [l] -> Type
type instance Apply (ConsMap0 f)    a = ConsMap1 f a
type instance Apply (ConsMap1 f a) tl = Apply f a ': tl

type family Constant (b :: l) (as :: [k]) :: [l] where
  Constant b as = Map (Constant1 b) as

------------------------------------------------------------------
-- TYPE FORMERS
------------------------------------------------------------------

-- | @Arrows [a1,..,an] r@ corresponds to @a1 -> .. -> an -> r@
-- | @Products [a1,..,an]@ corresponds to @(a1, (..,( an, ())..))@

type Arrows   (as :: [Type]) (r :: Type) = Foldr (->) r as
type Products (as :: [Type])             = Foldr (,) () as

-- | @IsBase t@ is @'True@ whenever @t@ is *not* a function space.

type family IsBase (t :: Type) :: Bool where
  IsBase (a -> t) = 'False
  IsBase a        = 'True

-- | Using @IsBase@ we can define notions of @Domains@ and @CoDomains@
--   which *reduce* under positive information @IsBase t ~ 'True@ even
--   though the shape of @t@ is not formally exposed

type family Domains (t :: Type) :: [Type] where
  Domains t = If (IsBase t) '[] (Domains' t)
type family Domains' (t :: Type) :: [Type] where
  Domains' (a -> t) = a ': Domains t

type family CoDomain (t :: Type) :: Type where
  CoDomain t = If (IsBase t) t (CoDomain' t)
type family CoDomain' (t :: Type) :: Type where
  CoDomain' (a -> t) = CoDomain t

------------------------------------------------------------------
-- TYPECLASS MAGIC
------------------------------------------------------------------

-- | @Currying as b@ witnesses the isomorphism between @Arrows as b@
--   and @Products as -> b@. It is defined as a type class rather
--   than by recursion on a singleton for @as@ so all of that these
--   conversions are inlined at compile time for concrete arguments.

class Currying as b where
  uncurrys :: Proxy as -> Proxy b -> Arrows as b -> Products as -> b
  currys   :: Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b

instance Currying '[] b where
  uncurrys :: Proxy '[] -> Proxy b -> Arrows '[] b -> Products '[] -> b
uncurrys Proxy '[]
_ Proxy b
_ Arrows '[] b
f = \ () -> b
Arrows '[] b
f
  currys :: Proxy '[] -> Proxy b -> (Products '[] -> b) -> Arrows '[] b
currys   Proxy '[]
_ Proxy b
_ Products '[] -> b
f = Products '[] -> b
f ()

instance Currying as b => Currying (a ': as) b where
  uncurrys :: Proxy (a : as)
-> Proxy b -> Arrows (a : as) b -> Products (a : as) -> b
uncurrys Proxy (a : as)
_ Proxy b
p Arrows (a : as) b
f = (a -> Foldr (,) () as -> b) -> (a, Foldr (,) () as) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((a -> Foldr (,) () as -> b) -> (a, Foldr (,) () as) -> b)
-> (a -> Foldr (,) () as -> b) -> (a, Foldr (,) () as) -> b
forall a b. (a -> b) -> a -> b
$ Proxy as -> Proxy b -> Foldr (->) b as -> Foldr (,) () as -> b
forall (as :: [*]) b.
Currying as b =>
Proxy as -> Proxy b -> Arrows as b -> Products as -> b
uncurrys (Proxy as
forall {k} (t :: k). Proxy t
Proxy :: Proxy as) Proxy b
p (Foldr (->) b as -> Foldr (,) () as -> b)
-> (a -> Foldr (->) b as) -> a -> Foldr (,) () as -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arrows (a : as) b
a -> Foldr (->) b as
f
  currys :: Proxy (a : as)
-> Proxy b -> (Products (a : as) -> b) -> Arrows (a : as) b
currys   Proxy (a : as)
_ Proxy b
p Products (a : as) -> b
f = Proxy as -> Proxy b -> (Foldr (,) () as -> b) -> Foldr (->) b as
forall (as :: [*]) b.
Currying as b =>
Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b
currys (Proxy as
forall {k} (t :: k). Proxy t
Proxy :: Proxy as) Proxy b
p ((Foldr (,) () as -> b) -> Foldr (->) b as)
-> (a -> Foldr (,) () as -> b) -> a -> Foldr (->) b as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Foldr (,) () as) -> b) -> a -> Foldr (,) () as -> b
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a, Foldr (,) () as) -> b
Products (a : as) -> b
f

------------------------------------------------------------------
-- DEFUNCTIONALISATION
-- Cf. Eisenberg and Stolarek's paper:
-- Promoting Functions to Type Families in Haskell
------------------------------------------------------------------

data Function :: Type -> Type -> Type

data Constant0 :: Function a (Function b a -> Type) -> Type
data Constant1 :: Type -> Function b a -> Type

type family Apply (t :: Function k l -> Type) (u :: k) :: l

type instance Apply Constant0     a = Constant1 a
type instance Apply (Constant1 a) b = a