sized_expr.jl

using MLStyle
import Base
@data Nat begin
    Z()
    S{N <: Nat} :: () => Nat
end

StoInt(s::Type{Z}) = 0
StoInt(s::Type{S{N}}) where N = StoInt(N) + 1

Base.show(io::IO, ::Type{N}) where N <: Nat = Base.show(io, StoInt(N))

@data SizedList{N <: Nat, T} begin
    ZL{T} :: () => SizedList{Z, T}
    SL{N, T} :: (T, SizedList{N, T}) => SizedList{S{N}, T}
end

abstract type MTag{N <: Nat} end
struct MExpr{N}
    head :: MTag{N}
    args :: SizedList{N, MExpr}
    MExpr(t :: MTag{N}, xs::MExpr...) where N = begin
        I = StoInt(N)
        T = Tuple{I, MExpr}
        args = mk_sized_mexpr_args(T, xs :: NTuple{I, T})
        new{N}(t, args)
    end
end

@inline function mk_sized_mexpr_args(::Type{Tuple{0, T}}, args::Tuple{}) where T
    ret = ZL{T}()
    for i = length(args):-1:1
        ret = SL(args[i], ret)
    end
    ret
end

@inline function mk_sized_mexpr_args(::Type{Tuple{N, T}}, args::NTuple{N, T}) where {N, T}
    ret = ZL{T}()
    for i = length(args):-1:1
        ret = SL(args[i], ret)
    end
    ret
end


const _0 = Z
const _1 = S{_0}
const _2 = S{_1}

@data MTag{N <: Nat} begin
    MForall :: MTag{_2}
    MLambda :: MTag{_2}
    MLet{N} :: SizedList{N, MExpr} => MTag{N}
    MBind   :: MTag{_2}
    MCall :: MExpr => MTag{_2}
    MSymbol :: Symbol => MTag{_0}
    MConst :: Any => MTag{0}
end

MExpr(MSymbol(:a))
MExpr(MLambda, MExpr(MSymbol(:a)), MExpr(MSymbol(:a)))
MExpr(MBind, MExpr(MSymbol(:a)), MExpr(MConst(:a)))