<commit_before>{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, KindSignatures #-}
{-# LANGUAGE GADTs #-}

-- |
-- Module      : Data.Type.RList
-- Copyright   : (c) 2016 <NAME>
--
-- License     : BSD3
--
-- Maintainer  : <EMAIL>
-- Stability   : experimental
-- Portability : GHC
--
-- A /right list/, or 'RList', is a list where cons adds to the end, or the
-- right-hand side, of a list. This is useful conceptually for contexts of
-- name-bindings, where the most recent name-binding is intuitively at the end
-- of the context.

module Data.Type.RList where

import Data.Type.Equality ((:~:)(..))
import Data.Proxy (Proxy(..))
import Data.Functor.Constant
import Data.Typeable

-------------------------------------------------------------------------------
-- Right-lists as a datatype
-------------------------------------------------------------------------------

data RList a
  = RNil
  | (RList a) :> a

type family ((r1 :: RList k) :++: (r2 :: RList k)) :: RList k
infixr 5 :++:
type instance (r :++: 'RNil) = r
type instance (r1 :++: (r2 ':> a)) = (r1 :++: r2) ':> a

proxyCons :: Proxy r -> f a -> Proxy (r :> a)
proxyCons _ _ = Proxy


-------------------------------------------------------------------------------
-- proofs of membership in a type-level list
-------------------------------------------------------------------------------

{-|
  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
  list @ctx@, meaning that @ctx@ equals

>  t0 ':>' a ':>' t1 ':>' ... ':>' tn

  for some types @t0,t1,...,tn@.
-}
data Member ctx a where
  Member_Base :: Member (ctx :> a) a
  Member_Step :: Member ctx a -> Member (ctx :> b) a
  deriving Typeable

instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)

showsPrecMember :: Bool -> Member ctx a -> ShowS
showsPrecMember _ Member_Base = showString "Member_Base"
showsPrecMember p (Member_Step prf) = showParen p $
  showString "Member_Step" . showsPrec 10 prf

--toEq :: Member (Nil :> a) b -> b :~: a
--toEq Member_Base = Refl
--toEq _ = error "Should not happen! (toEq)"

weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
weakenMemberL _ Member_Base = Member_Base
weakenMemberL tag (Member_Step mem) = Member_Step (weakenMemberL tag mem)

membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
membersEq Member_Base Member_Base = Just Refl
membersEq (Member_Step mem1) (Member_Step mem2) = membersEq mem1 mem2<commit_msg>added explicit kind annotations to Member, to allow (uninhabied) Member proofs for different-kinded contexts and elements<commit_after>{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, KindSignatures #-}
{-# LANGUAGE GADTs #-}

-- |
-- Module      : Data.Type.RList
-- Copyright   : (c) 2016 <NAME>
--
-- License     : BSD3
--
-- Maintainer  : <EMAIL>
-- Stability   : experimental
-- Portability : GHC
--
-- A /right list/, or 'RList', is a list where cons adds to the end, or the
-- right-hand side, of a list. This is useful conceptually for contexts of
-- name-bindings, where the most recent name-binding is intuitively at the end
-- of the context.

module Data.Type.RList where

import Data.Type.Equality ((:~:)(..))
import Data.Proxy (Proxy(..))
import Data.Functor.Constant
import Data.Typeable

-------------------------------------------------------------------------------
-- Right-lists as a datatype
-------------------------------------------------------------------------------

data RList a
  = RNil
  | (RList a) :> a

type family ((r1 :: RList k) :++: (r2 :: RList k)) :: RList k
infixr 5 :++:
type instance (r :++: 'RNil) = r
type instance (r1 :++: (r2 ':> a)) = (r1 :++: r2) ':> a

proxyCons :: Proxy r -> f a -> Proxy (r :> a)
proxyCons _ _ = Proxy


-------------------------------------------------------------------------------
-- proofs of membership in a type-level list
-------------------------------------------------------------------------------

{-|
  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
  list @ctx@, meaning that @ctx@ equals

>  t0 ':>' a ':>' t1 ':>' ... ':>' tn

  for some types @t0,t1,...,tn@.
-}
data Member (ctx :: RList k1) (a :: k2) where
  Member_Base :: Member (ctx :> a) a
  Member_Step :: Member ctx a -> Member (ctx :> b) a
  deriving Typeable

instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)

showsPrecMember :: Bool -> Member ctx a -> ShowS
showsPrecMember _ Member_Base = showString "Member_Base"
showsPrecMember p (Member_Step prf) = showParen p $
  showString "Member_Step" . showsPrec 10 prf

--toEq :: Member (Nil :> a) b -> b :~: a
--toEq Member_Base = Refl
--toEq _ = error "Should not happen! (toEq)"

weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
weakenMemberL _ Member_Base = Member_Base
weakenMemberL tag (Member_Step mem) = Member_Step (weakenMemberL tag mem)

membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
membersEq Member_Base Member_Base = Just Refl
membersEq (Member_Step mem1) (Member_Step mem2) = membersEq mem1 mem2
{'fraction_non_alphanumeric': 0.2509742790335152, 'fraction_numerical': 0.011301636788776305, 'mean_word_length': 2.0663082437275984, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 53, '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': '1422627', 'n_tokens_mistral': 1678, 'n_tokens_neox': 1608, 'n_words': 565}