<commit_before>{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, RankNTypes,
  MultiParamTypeClasses #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Param.Term
-- Copyright   :  (c) 2011 <NAME>, <NAME>
-- License     :  BSD3
-- Maintainer  :  <NAME> <<EMAIL>>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines the central notion of /parametrized terms/ and their
-- generalisation to parametrised contexts.
--
--------------------------------------------------------------------------------

module Data.Comp.Param.Term
    (
     Cxt(..),
     Hole,
     NoHole,
     Any,
     Term,
     Context,
     Const,
     simpCxt,
     coerceCxt,
     toCxt,
     constTerm
    ) where

import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
import Data.Comp.Param.Difunctor
import Data.Comp.Param.Ditraversable
import Data.Maybe (fromJust)
import Unsafe.Coerce

{-| This data type represents contexts over a signature. Contexts are terms
  containing zero or more holes, and zero or more parameters. The first
  parameter is a phantom type indicating whether the context has holes. The
  second paramater is the signature of the context, in the form of a
  "Data.Comp.Param.Difunctor". The third parameter is the type of parameters,
  and the fourth parameter is the type of holes. -}
data Cxt :: * -> (* -> * -> *) -> * -> * -> * where
            Term :: f a (Cxt h f a b) -> Cxt h f a b
            Hole :: b -> Cxt Hole f a b
            Place :: a -> Cxt h f a b

{-| Phantom type used to define 'Context'. -}
data Hole

{-| Phantom type used to define 'Term'. -}
data NoHole

{-| An empty type. @Any@ is used to emulate parametricity, e.g. a function of
  type @Any -> T[Any]@ is equivalent with @forall b. b -> T[b]@, but the
  former avoids the impredicative typing extension, and works also in the
  cases where the codomain type is not a type constructor, e.g.
  @Any -> (Any,Any)@. -}
data Any

instance Eq Any where
instance Ord Any where
instance Show Any where

{-| A context may contain holes, but must be parametric in the bound
  parameters. -}
type Context f = Cxt Hole f Any

{-| A term is a context with no holes, where all occurrences of the
  contravariant parameter is fully parametric. The type approximates the
  type @forall h a b. Cxt h f a b@ using the empty data types 'Any' and
  'NoHole', thereby avoiding impredicative types. -}
type Term f = Cxt NoHole f Any ()<commit_msg>Removed incorrect instances for the 'Any' type<commit_after>{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, RankNTypes,
  MultiParamTypeClasses #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Param.Term
-- Copyright   :  (c) 2011 <NAME>, <NAME>
-- License     :  BSD3
-- Maintainer  :  <NAME> <<EMAIL>>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines the central notion of /parametrized terms/ and their
-- generalisation to parametrised contexts.
--
--------------------------------------------------------------------------------

module Data.Comp.Param.Term
    (
     Cxt(..),
     Hole,
     NoHole,
     Any,
     Term,
     Context,
     Const,
     simpCxt,
     coerceCxt,
     toCxt,
     constTerm
    ) where

import Prelude hiding (mapM, sequence, foldl, foldl1, foldr, foldr1)
import Data.Comp.Param.Difunctor
import Data.Comp.Param.Ditraversable
import Data.Maybe (fromJust)
import Unsafe.Coerce

{-| This data type represents contexts over a signature. Contexts are terms
  containing zero or more holes, and zero or more parameters. The first
  parameter is a phantom type indicating whether the context has holes. The
  second paramater is the signature of the context, in the form of a
  "Data.Comp.Param.Difunctor". The third parameter is the type of parameters,
  and the fourth parameter is the type of holes. -}
data Cxt :: * -> (* -> * -> *) -> * -> * -> * where
            Term :: f a (Cxt h f a b) -> Cxt h f a b
            Hole :: b -> Cxt Hole f a b
            Place :: a -> Cxt h f a b

{-| Phantom type used to define 'Context'. -}
data Hole

{-| Phantom type used to define 'Term'. -}
data NoHole

{-| An empty type. @Any@ is used to emulate parametricity, e.g. a function of
  type @Any -> T[Any]@ is equivalent with @forall b. b -> T[b]@, but the
  former avoids the impredicative typing extension, and works also in the
  cases where the codomain type is not a type constructor, e.g.
  @Any -> (Any,Any)@. -}
data Any

{-| A context may contain holes, but must be parametric in the bound
  parameters. -}
type Context f = Cxt Hole f Any

{-| A term is a context with no holes, where all occurrences of the
  contravariant parameter is fully parametric. The type approximates the
  type @forall h a b. Cxt h f a b@ using the empty data types 'Any' and
  'NoHole', thereby avoiding impredicative types. -}
type Term f = Cxt NoHole f Any ()
{'fraction_non_alphanumeric': 0.15692490588468397, 'fraction_numerical': 0.0027739251040221915, 'mean_word_length': 2.235897435897436, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 37, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7219967', 'n_tokens_mistral': 1534, 'n_tokens_neox': 1487, 'n_words': 630}