Type level functions for Agda's Utils library

Agda.Utils.TypeLevel.hs

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE ScopedTypeVariables  #-}
-- 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.Proxy
import Data.Kind (Constraint)
import Data.Constraint
import GHC.TypeLits

------------------------------------------------------------------
-- 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)

type family Foldr' (c :: Function k (Function l l -> *) -> *)
                   (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 -> *) (as :: [k]) :: [l] where
  Map f as = Foldr' (ConsMap0 f) '[] as

data ConsMap0 :: (Function k l -> *) -> Function k (Function [l] [l] -> *) -> *
data ConsMap1 :: (Function k l -> *) -> k -> Function [l] [l] -> *
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 :: [*]) (r :: *) = Foldr ((->)) r as
type Products (as :: [*])          = Foldr (,) () as

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

type family IsBase (t :: *) :: 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 :: *) :: [*] where
  Domains t = If (IsBase t) '[] (Domains' t)
type family Domains' (t :: *) :: [*] where
  Domains' (a -> t) = a : Domains t

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

------------------------------------------------------------------
-- SINGLETONS
-- To break down and inspect type-level constructs, we need value
-- level GADTs exposing their structure.
------------------------------------------------------------------

-- | @STList as@ is a value-level list containing a @Proxy a@
--   for each @a@ in @as@.

data STList (as :: [k]) :: * where
  STNil  :: STList '[]
  STCons :: Proxy a -> STList as -> STList (a ': as)

-- | @currys@ and @uncurrys@ witness the isomorphism between
--   @Arrows as r@ and @Product as -> r@

currys :: STList as -> (Products as -> r) -> Arrows as r
currys STNil          f = f ()
currys (STCons _ stl) f = currys stl . curry f

uncurrys :: STList as -> Arrows as r -> (Products as -> r)
uncurrys STNil          f = const f
uncurrys (STCons _ stl) f = uncurry $ uncurrys stl . f

mapSTL :: Proxy f -> STList as -> STList (Map f as)
mapSTL _ STNil          = STNil
mapSTL p (STCons _ stl) = STCons Proxy $ mapSTL p stl

-- | @constant@ witnesses the fact that if we have a singleton
--   @STList as@ for @as@, we can get one for @Constant b as@

constant :: forall (b :: *) as. Proxy b -> STList as -> STList (Constant b as)
constant p = mapSTL (Proxy :: Proxy (Constant1 b))

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

-- | @Reify t (IsBase t)@ traverses @t@ to produce a proof that it
--   can be split between its @Domains@ (of which we get a singleton)
--   and its @CoDomain@.
--   The @IsBase t@ extra argument to the type class guarantees that
--   the two instances are non-overlapping.

class Reify t b where
  reify :: b ~ IsBase t => Proxy t ->
           (STList (Domains t), Dict (t ~ Arrows (Domains t) (CoDomain t)))

instance Reify t 'True where
  reify _ = (STNil, Dict)

instance Reify t (IsBase t) => Reify (a -> t) 'False where
  reify _ = case reify (Proxy :: Proxy t) of
    (stl, Dict) -> (STCons (Proxy :: Proxy a) stl, Dict)



------------------------------------------------------------------
-- DEFUNCTIONALISATION
------------------------------------------------------------------

data Function :: * -> * -> *

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

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

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