{-# 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 :: forall a (as :: [*]). HList (a : as) -> a
hHead (anyTy
x `HCons` HList manyTys
_) = anyTy
x
hOf :: forall y xs . IsInProof y xs => Proxy y -> HList xs -> y
hOf :: forall y (xs :: [*]). IsInProof y xs => Proxy y -> HList xs -> y
hOf Proxy y
proxy = forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy y
proxy forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn
where
go :: Proxy x -> IsIn x ys -> HList ys -> x
go :: forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy x
_ IsIn x ys
IsHead (anyTy
y `HCons` HList manyTys
_) = anyTy
y
go Proxy x
pxy (IsInTail IsIn x tys
cons) (anyTy
_ `HCons` HList manyTys
rest) = forall x (ys :: [*]). Proxy x -> IsIn x ys -> HList ys -> x
go Proxy x
pxy IsIn x tys
cons 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)
&: :: forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
(&:) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
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) = forall a. Show a => a -> String
show anyTy
x forall a. [a] -> [a] -> [a]
++ String
" &: " forall a. [a] -> [a] -> [a]
++ 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 forall a. Eq a => a -> a -> Bool
== anyTy
y Bool -> Bool -> Bool
&& HList manyTys
xs forall a. Eq a => a -> a -> Bool
== 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 = forall (k :: Symbol) t (tys :: [*]). LookupKV k t (KV k t : tys)
AtHead @k @t @'[]
instance {-# Overlapping #-} MemberKV k t (KV k t ': kvs) where
lookupProof :: LookupKV k t (KV k t : kvs)
lookupProof = forall (k :: Symbol) t (tys :: [*]). LookupKV k t (KV k t : tys)
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 = forall (k :: Symbol) t (tys :: [*]) (otherTy :: Symbol) ot.
LookupKV k t tys -> LookupKV k t (KV otherTy ot : tys)
OtherKeys 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 :: forall (k :: Symbol) t (xs :: [*]).
MemberKV k t xs =>
HList xs -> t
select = forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go forall a b. (a -> b) -> a -> b
$ 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 :: forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 xs1
AtHead (V t1
x `HCons` HList manyTys
_) = t1
x
go (OtherKeys LookupKV k1 t1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = forall (k1 :: Symbol) t1 (xs1 :: [*]).
LookupKV k1 t1 xs1 -> HList xs1 -> t1
go LookupKV k1 t1 kvs
cons 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 = 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 = forall (tys :: [Symbol]) (otherTy :: [*]) (ot :: [*]) (k :: Symbol)
t.
LookupMany tys otherTy ot
-> LookupMany (k : tys) (t : otherTy) (KV k t : ot)
NextOfMany 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 = forall (ks :: [Symbol]) (ts :: [*]) (tys :: [*])
(otherTy :: Symbol) ot.
LookupMany ks ts tys -> LookupMany ks ts (KV otherTy ot : tys)
ManyOthers 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 :: forall (ks :: [Symbol]) (ts :: [*]) (xs :: [*]).
ManyMemberKV ks ts xs =>
HList xs -> HList ts
selectMany = forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go forall a b. (a -> b) -> a -> b
$ 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 :: forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 xs1
FirstOfMany (V t
x `HCons` HList manyTys
_) = t
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil
go (NextOfMany LookupMany ks ts kvs
cons) (V t
x `HCons` HList manyTys
y) = t
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks ts kvs
cons HList manyTys
y
go (ManyOthers LookupMany ks1 ts1 kvs
cons) (anyTy
_ `HCons` HList manyTys
y) = forall (ks1 :: [Symbol]) (ts1 :: [*]) (xs1 :: [*]).
LookupMany ks1 ts1 xs1 -> HList xs1 -> HList ts1
go LookupMany ks1 ts1 kvs
cons 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 = forall y (xs :: [*]). IsInProof y xs => Proxy y -> HList xs -> y
hOf @y forall {k} (t :: k). Proxy t
Proxy HList xs
xs forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` 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 = 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 = forall t (tys :: [*]) otherTy. IsIn t tys -> IsIn t (otherTy : tys)
IsInTail forall t (tys :: [*]). IsInProof t tys => IsIn t tys
provedIsIn