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 -- * Type 'Type_Root'
  16 -- | The root type, passing itself as parameter to the given type.
  17 newtype Type_Root (ty:: (* -> *) -> * -> *) h
  18  =      Type_Root { unType_Root :: ty (Type_Root ty) h }
  19 type instance Root_of_Type (Type_Root ty) = Type_Root ty
  20
  21 -- ** Type family 'Root_of_Type'
  22 -- | Return the root type of a type.
  23 type family Root_of_Type (ty:: * -> *) :: * -> *
  24
  25 -- ** Class 'Type_Root_Lift'
  26 -- | Lift a given type to a given root type.
  27 class Type_Root_Lift ty root where
  28         type_root_lift :: forall h. ty root h -> root h
  29