{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Type.Index
-- Copyright : Copyright (C) 2015 Kyle Carter
-- License : BSD3
--
-- Maintainer : Kyle Carter <kylcarte@indiana.edu>
-- Stability : experimental
-- Portability : RankNTypes
--
-- A @singleton@-esque type for representing indices in a type-level list.
--
-----------------------------------------------------------------------------
module Data.Type.Index where
-- import Data.Type.Quantifier
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.List
data Index :: [k] -> k -> * where
IZ :: Index (a :< as) a
IS :: !(Index as a) -> Index (b :< as) a
deriving instance Eq (Index as a)
deriving instance Ord (Index as a)
deriving instance Show (Index as a)
instance Eq1 (Index as)
instance Ord1 (Index as)
instance Show1 (Index as)
instance Read2 Index where
readsPrec2 d = readParen (d > 10) $ \s0 ->
[ (Some2 IZ,s1)
| ("IZ",s1) <- lex s0
] ++
[ (i >>-- Some2 . IS,s2)
| ("IS",s1) <- lex s0
, (i,s2) <- readsPrec2 11 s1
]
instance TestEquality (Index as) where
testEquality = \case
IZ -> \case
IZ -> qed
_ -> Nothing
IS x -> \case
IS y -> x =?= y //? qed
_ -> Nothing
elimIndex :: (forall xs. p (a :< xs) a)
-> (forall x xs. Index xs a -> p xs a -> p (x :< xs) a)
-> Index as a
-> p as a
elimIndex z s = \case
IZ -> z
IS x -> s x $ elimIndex z s x
ixNil :: Index Ø a -> b
ixNil = absurd . impossible
onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a
onIxPred f = \case
IZ -> IZ
IS x -> IS $ f x
type a ∈ as = Elem as a
infix 6 ∈
class Elem (as :: [k]) (a :: k) where
elemIndex :: Index as a
instance {-# OVERLAPPING #-} Elem (a :< as) a where
elemIndex = IZ
instance {-# OVERLAPPABLE #-} Elem as a => Elem (b :< as) a where
elemIndex = IS elemIndex
instance Witness ØC (Elem as a) (Index as a) where
(\\) r = \case
IZ -> r
IS x -> r \\ x
instance (a ∈ as) => Known (Index as) a where
type KnownC (Index as) a = (a ∈ as)
known = elemIndex
class EveryC c as => Every (c :: k -> Constraint) (as :: [k]) where
type EveryC c as :: Constraint
every :: Index as a -> Wit (c a)
instance Every c Ø where
type EveryC c Ø = ØC
every = ixNil
instance (c a, Every c as) => Every c (a :< as) where
type EveryC c (a :< as) = (c a, Every c as)
every = \case
IZ -> Wit
IS x -> every x
class ListC ((c <$> xs) <&> y)
=> Every2 (c :: k -> l -> Constraint) (xs :: [k]) (y :: l) where
every2 :: Index xs x -> Wit (c x y)
instance Every2 c Ø y where
every2 = ixNil
instance (c x y, Every2 c xs y) => Every2 c (x :< xs) y where
every2 = \case
IZ -> Wit
IS x -> every2 x