Language/Symantic/Type/Root.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 module Language.Symantic.Type.Root where
  14
  15
  16 -- * Type 'Type_Root'
  17 -- | The root type, passing itself as parameter to the given type.
  18 newtype Type_Root (ty:: (* -> *) -> * -> *) h
  19  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
  20 type instance Root_of_Type (Type_Root ty) = Type_Root ty
  21
  22 -- ** Type family 'Root_of_Type'
  23 -- | Return the root type of a type.
  24 type family Root_of_Type (ty:: * -> *) :: * -> *
  25
  26 -- ** Class 'Lift_Type_Root'
  27 -- | Lift a given type to a given root type.
  28 class Lift_Type_Root ty root where
  29         lift_type_root :: forall h. ty root h -> root h
  30