Portability | see LANGUAGE pragmas (... GHC) |
---|---|
Stability | experimental |
Maintainer | nicolas.frisby@gmail.com |
Finite sums of types.
Documentation
(Med m (LeftmostRange ts) ~ Med m (LeftmostRange us), Reduce m ts, Reduce m us) => Reduce m (:+ ts us) | |
(c ::: (All u), d ::: (All u)) => (:+ c d) ::: (All u) | |
d ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnRight path)) | |
c ::: (:? (Exists p) path) => (:+ c d) ::: (:? (Exists p) (OnLeft path)) |
The higher-order universe All
. c
inhabits All u
if c
is a type-sum
and all types in it inhabit u
.
The higher-order universe Exists
. c
inhabits Exists p
if there
exists a type t
in the type-sum c
for which
. NB
that True
~ Pred
p tc
is not necessarily a type-sum; i.e. there is no well-typed total
function from Exists p c
to TSum c
.