Dependent sums subsume algebraic data types in presence of enums

NatSum.idr

%hide Nat
%hide Nat.S
%hide Nat.Z

function : List Type -> Type -> Type
function [] b = b
function (a :: as) b = a -> function as b

infixr 10 *->

(*->) : List Type -> Type -> Type
(*->) = function

tuple : List Type -> Type
tuple [] = ()
tuple (a :: as) = (a, tuple as)

map : (a -> b) -> (args *-> a) -> (args *-> b)
map f {args=[]}        z = f z
map f {args=(a :: as)} g = \x => map f (g x)

tupleConstructor : (args : List Type) -> args *-> (tuple args)
tupleConstructor [] = ()
tupleConstructor (a :: as) = \x => map (\xs => (x, xs)) (tupleConstructor as)

tupleEliminator : tuple args -> (args *-> a) -> a
tupleEliminator {args=[]}        ()      z = z
tupleEliminator {args=(a :: as)} (x, xs) g = tupleEliminator xs (g x)

--

%auto_implicits off 
record AlgebraicData (Tag : Type) (Payload : Tag -> List Type) where
    constructor MkAlgebraicDataRaw
    tag : Tag
    payload : tuple (Payload tag)
%auto_implicits on 

MkAlgebraicData : {Tag : _, Payload : _} -> (tag : Tag) -> Payload tag *-> AlgebraicData Tag Payload
MkAlgebraicData tag {Payload} = map (MkAlgebraicDataRaw tag) (tupleConstructor (Payload tag))

prefix 1 #

(#) : {Tag : _, Payload : _} -> (tag : Tag) -> Payload tag *-> AlgebraicData Tag Payload
(#) = MkAlgebraicData

elimAlgebraicData : {Tag : _, Payload : _} -> ((tag : Tag) -> Payload tag *-> a) -> AlgebraicData Tag Payload  -> a
elimAlgebraicData eliminator (MkAlgebraicDataRaw tag payload) = tupleEliminator payload (eliminator tag)

--

mutual
    data NatTag = Z | S

    NatPayload : NatTag -> List Type
    NatPayload Z = []
    NatPayload S = [Nat]

    Nat : Type
    Nat = AlgebraicData NatTag NatPayload
    
    MkNat : (tag : NatTag) -> NatPayload tag *-> Nat
    MkNat = MkAlgebraicData
    
    elimNat : ((tag : NatTag) -> NatPayload tag *-> a) -> Nat -> a
    elimNat = elimAlgebraicData
    
{- commented out due to Idris type system bug
three : Nat
three = #S (#S (#S (#Z)))

double : Nat -> Nat
double = elimNat double'
    where double' : (tag : NatTag) -> NatPayload tag *-> (AlgebraicData NatTag NatPayload)
          double' Z   = #Z
          double' S x = #S (#S (double x))
-}