CPSifying Sigma seems to suffer from the same issue as lambda encoding of any inductive type, which is self reference.
The lambda encodings of inductive types can be solved by using self types, instead of declaring unit using the traditional church encoding, by using self types we self encode the induction principle, allowing to be known that (u : Unit) -> u == unit.
// traditional church encoding of unit, no induction
Unit : Type;
unit : Unit;
Unit = (A : Type) -> (x : A) -> A;
unit = A => x => x;
// self dependent encoding of unit, inductive
Unit : Type;
unit : Unit;
Unit = %self(u). (P : Unit -> Type) -> P unit -> P u;
unit = P => x => x;Instead of doing the traditional polymorphic CPS version, we can do a self referential CPS version
// original
x : A;
x = e;
// traditional CPS polymorphic
CPS : (A : Type) -> Type;
CPS = A => (K : Type) -> (k : (x : A) -> Type) -> K;
x : CPS A;
x = K => k => k e;
// self referential version
CPS : (A : Type) -> Type;
CPS = A => %self(x). (K : CPS A -> Type) ->
(k : (y : T) -> K (K => k => k y)) -> K x;
x : CPS A;
x = K => k => k e;This allows to transform any external callback.
example : B (fst x)
example = x (a => B (fst a)) (y => snd y);