{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK prune not-home #-}
module System.TmpProc.TypeLevel
(
HList(..)
, (&:)
, hHead
, hOf
, ReorderH(..)
, KV(..)
, select
, selectMany
, LookupKV(..)
, MemberKV(..)
, ManyMemberKV(..)
, IsAbsent
, IsInProof
, module System.TmpProc.TypeLevel.Sort
)
where
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import GHC.Exts (Constraint)
import GHC.TypeLits (ErrorMessage (..), Symbol,
TypeError)
import qualified GHC.TypeLits as TL
import System.TmpProc.TypeLevel.Sort
hHead :: HList (a ': as) -> a
hHead :: HList (a : as) -> a
hHead (anyTy
x `HCons` HList manyTys
_) = a
anyTy
x
hOf :: forall y xs . IsInProof y xs => Proxy y -> HList xs -> y
hOf :: Proxy y -> HList xs -> y
hOf Proxy y
proxy = Proxy y -> IsIn y xs -> HList xs -> y
forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy y
proxy IsIn y xs
forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn
where
go :: Proxy x -> IsIn x ys -> HList ys -> x
go :: Proxy x -> IsIn x ys -> HList ys -> x
go Proxy x
_ IsIn x ys
IsHead (anyTy
y `HCons` HList manyTys
_) = x
anyTy
y
go Proxy x
pxy (IsInTail IsIn x tys
cons) (anyTy
_ `HCons` HList manyTys
rest) = Proxy x -> IsIn x tys -> HList tys -> x
forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy x
pxy IsIn x tys
cons HList tys
HList manyTys
rest
data HList :: [*] -> * where
HNil :: HList '[]
HCons :: anyTy -> HList manyTys -> HList (anyTy ': manyTys)
infixr 5 `HCons`
infixr 5 &:
(&:) :: x -> HList xs -> HList (x ': xs)
&: :: x -> HList xs -> HList (x : xs)
(&:) = x -> HList xs -> HList (x : xs)
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
HCons
instance Show (HList '[]) where
show :: HList '[] -> String
show HList '[]
HNil = String
"HNil"
instance (Show x, Show (HList xs)) => Show (HList (x ': xs)) where
show :: HList (x : xs) -> String
show (HCons anyTy
x HList manyTys
xs) = anyTy -> String
forall a. Show a => a -> String
show anyTy
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" &: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ HList manyTys -> String
forall a. Show a => a -> String
show HList manyTys
xs
instance Eq (HList '[]) where
HList '[]
HNil == :: HList '[] -> HList '[] -> Bool
== HList '[]
HNil = Bool
True
instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs)) where
(HCons anyTy
x HList manyTys
xs) == :: HList (x : xs) -> HList (x : xs) -> Bool
== (HCons anyTy
y HList manyTys
ys) = anyTy
x anyTy -> anyTy -> Bool
forall a. Eq a => a -> a -> Bool
== anyTy
anyTy
y Bool -> Bool -> Bool
&& HList manyTys
xs HList manyTys -> HList manyTys -> Bool
forall a. Eq a => a -> a -> Bool
== HList manyTys
HList manyTys
ys
data KV :: Symbol -> * -> * where
V :: a -> KV s a
type family IsAbsent e r :: Constraint where
IsAbsent e '[] = ()
IsAbsent e (e ': _) = TypeError (NotAbsentErr e)
IsAbsent e (e' ': tail) = IsAbsent e tail
type NotAbsentErr e =
('TL.Text " type " ':<>: 'TL.ShowType e) ':<>:
('TL.Text " is already in this type list, and is not allowed again")
data LookupKV (k :: Symbol) t (xs :: [*]) where
AtHead :: LookupKV k t (KV k t ': kvs)
OtherKeys :: LookupKV k t kvs -> LookupKV k t (KV ok ot ': kvs)
class MemberKV (k :: Symbol) (t :: *) (xs :: [*]) where
lookupProof :: LookupKV k t xs
instance {-# Overlapping #-} MemberKV k t '[KV k t] where
lookupProof :: LookupKV k t '[KV k t]
lookupProof = LookupKV k t '[KV k t]
forall (k :: Symbol) t (kvs :: [*]). LookupKV k t (KV k t : kvs)
AtHead @k @t @'[]
instance {-# Overlapping #-} MemberKV k t (KV k t ': kvs) where
lookupProof :: LookupKV k t (KV k t : kvs)
lookupProof = LookupKV k t (KV k t : kvs)
forall (k :: Symbol) t (kvs :: [*]). LookupKV k t (KV k t : kvs)
AtHead @k @t @kvs
instance MemberKV k t kvs => MemberKV k t (KV ok ot ': kvs) where
lookupProof :: LookupKV k t (KV ok ot : kvs)
lookupProof = LookupKV k t kvs -> LookupKV k t (KV ok ot : kvs)
forall (k :: Symbol) t (kvs :: [*]) (ok :: Symbol) ot.
LookupKV k t kvs -> LookupKV k t (KV ok ot : kvs)
OtherKeys LookupKV k t kvs
forall (k :: Symbol) t (xs :: [*]).
MemberKV k t xs =>
LookupKV k t xs
lookupProof
select
:: forall k t xs . MemberKV k t xs
=> HList xs
-> t
select :: HList xs -> t
select = LookupKV k t xs -> HList xs -> t
forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go (LookupKV k t xs -> HList xs -> t)
-> LookupKV k t xs -> HList xs -> t
forall a b. (a -> b) -> a -> b
$ MemberKV k t xs => LookupKV k t xs
forall (k :: Symbol) t (xs :: [*]).
MemberKV k t xs =>
LookupKV k t xs
lookupProof @k @t @xs
where
go :: LookupKV k1 t1 xs1 -> HList xs1 -> t1
go :: LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 xs1
AtHead (V x `HCons` HList manyTys
_) = t1
x
go (OtherKeys LookupKV k1 t1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = LookupKV k1 t1 kvs -> HList kvs -> t1
forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 kvs
cons HList kvs
HList manyTys
y
data LookupMany (keys :: [Symbol]) (t :: [*]) (xs :: [*]) where
FirstOfMany :: LookupMany (k ': '[]) (t ': '[]) (KV k t ': kvs)
NextOfMany
:: LookupMany ks ts kvs
-> LookupMany (k ': ks) (t ': ts) (KV k t ': kvs)
ManyOthers :: LookupMany ks ts kvs -> LookupMany ks ts (KV ok ot ': kvs)
class ManyMemberKV (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]) where
manyProof :: LookupMany ks ts kvs
instance {-# Overlapping #-} ManyMemberKV '[k] '[t] (KV k t ': ks) where
manyProof :: LookupMany '[k] '[t] (KV k t : ks)
manyProof = LookupMany '[k] '[t] (KV k t : ks)
forall (k :: Symbol) t (ks :: [*]).
LookupMany '[k] '[t] (KV k t : ks)
FirstOfMany @k @t @ks
instance {-# Overlapping #-} ManyMemberKV ks ts kvs => ManyMemberKV (k ': ks) (t ': ts) (KV k t ': kvs) where
manyProof :: LookupMany (k : ks) (t : ts) (KV k t : kvs)
manyProof = LookupMany ks ts kvs -> LookupMany (k : ks) (t : ts) (KV k t : kvs)
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]) (k :: Symbol) t.
LookupMany ks ts kvs -> LookupMany (k : ks) (t : ts) (KV k t : kvs)
NextOfMany LookupMany ks ts kvs
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]).
ManyMemberKV ks ts kvs =>
LookupMany ks ts kvs
manyProof
instance ManyMemberKV ks ts kvs => ManyMemberKV ks ts (KV ok ot ': kvs) where
manyProof :: LookupMany ks ts (KV ok ot : kvs)
manyProof = LookupMany ks ts kvs -> LookupMany ks ts (KV ok ot : kvs)
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]) (ok :: Symbol) ot.
LookupMany ks ts kvs -> LookupMany ks ts (KV ok ot : kvs)
ManyOthers LookupMany ks ts kvs
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]).
ManyMemberKV ks ts kvs =>
LookupMany ks ts kvs
manyProof
selectMany
:: forall ks ts xs . ManyMemberKV ks ts xs
=> HList xs
-> HList ts
selectMany :: HList xs -> HList ts
selectMany = LookupMany ks ts xs -> HList xs -> HList ts
forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go (LookupMany ks ts xs -> HList xs -> HList ts)
-> LookupMany ks ts xs -> HList xs -> HList ts
forall a b. (a -> b) -> a -> b
$ ManyMemberKV ks ts xs => LookupMany ks ts xs
forall (ks :: [Symbol]) (ts :: [*]) (kvs :: [*]).
ManyMemberKV ks ts kvs =>
LookupMany ks ts kvs
manyProof @ks @ts @xs
where
go :: LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go :: LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 xs1
FirstOfMany (V x `HCons` HList manyTys
_) = t
x t -> HList '[] -> HList '[t]
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
`HCons` HList '[]
HNil
go (NextOfMany LookupMany ks ts kvs
cons) (V x `HCons` HList manyTys
y) = t
x t -> HList ts -> HList (t : ts)
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
`HCons` LookupMany ks ts kvs -> HList kvs -> HList ts
forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks ts kvs
cons HList kvs
HList manyTys
y
go (ManyOthers LookupMany ks1 ts1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = LookupMany ks1 ts1 kvs -> HList kvs -> HList ts1
forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 kvs
cons HList kvs
HList manyTys
y
class ReorderH xs ys where
hReorder :: HList xs -> HList ys
instance ReorderH xs '[] where
hReorder :: HList xs -> HList '[]
hReorder HList xs
_ = HList '[]
HNil
instance (IsInProof y xs, ReorderH xs ys) => ReorderH xs (y ': ys) where
hReorder :: HList xs -> HList (y : ys)
hReorder HList xs
xs = Proxy y -> HList xs -> y
forall y (xs :: [*]). IsInProof y xs => Proxy y -> HList xs -> y
hOf @y Proxy y
forall k (t :: k). Proxy t
Proxy HList xs
xs y -> HList ys -> HList (y : ys)
forall anyTy (manyTys :: [*]).
anyTy -> HList manyTys -> HList (anyTy : manyTys)
`HCons` HList xs -> HList ys
forall (xs :: [*]) (ys :: [*]).
ReorderH xs ys =>
HList xs -> HList ys
hReorder HList xs
xs
data IsIn t (xs :: [Type]) where
IsHead :: IsIn t (t ': tys)
IsInTail :: IsIn t tys -> IsIn t (otherTy ': tys)
class IsInProof t (tys :: [Type]) where
provedIsIn :: IsIn t tys
instance {-# Overlapping #-} IsInProof t (t ': tys) where
provedIsIn :: IsIn t (t : tys)
provedIsIn = IsIn t (t : tys)
forall t (tys :: [*]). IsIn t (t : tys)
IsHead @t @tys
instance IsInProof t tys => IsInProof t (a : tys) where
provedIsIn :: IsIn t (a : tys)
provedIsIn = IsIn t tys -> IsIn t (a : tys)
forall t (tys :: [*]) otherTy. IsIn t tys -> IsIn t (otherTy : tys)
IsInTail IsIn t tys
forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn