Nat.cs

#nullable enable

using System;

// ---

interface Hk<W, A> { }

// ---

static class Nat
{
  public static Nat_Z Z() => new Nat_Z();

  public static Nat_S<N> S<N>(this N prev)
    where N : Nat<N>
    => new Nat_S<N>(prev);

  public static Nat<N> Narrow<N>(this Hk<Nat_Mu, N> hk)
      where N : Nat<N>
          => (Nat<N>)hk;

  public static TyEq<Nat_S<N>, Nat_S<M>> Succ<N, M>(this TyEq<N, M> ty)
      where N : Nat<N>
      where M : Nat<M>
      => new TyEq_Trust<Nat_S<N>, Nat_S<M>>();

  public static TyEq<N, M> Prev<N, M>(this TyEq<Nat_S<N>, Nat_S<M>> ty)
      where N : Nat<N>
      where M : Nat<M>
      => new TyEq_Trust<N, M>();
}

//

abstract record Nat<N>() : Hk<Nat_Mu, N>
    where N : Nat<N>
{
  public abstract R Accept<R>(Nat_Visitor<R, N> visitor);

  public abstract Fin<N>? ToFin(uint value);

  public abstract TyEq<N, M>? Equals<M>(Nat<M> other)
    where M : Nat<M>;

  public abstract uint ToUInt();
}

interface Nat_Mu { }

//

sealed record Nat_Z() : Nat<Nat_Z>
{
  public override R Accept<R>(Nat_Visitor<R, Nat_Z> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_Z>(), this);

  public override Fin<Nat_Z>? ToFin(uint value)
    => null;

  public override TyEq<Nat_Z, M>? Equals<M>(Nat<M> other)
    => other.Accept<TyEq<Nat_Z, M>?>(new Nat_Z_Equals_Visitor<M>());

  public override uint ToUInt() => 0;
}

sealed record Nat_Z_Equals_Visitor<M>() : Nat_Visitor<TyEq<Nat_Z, M>?, M>
    where M : Nat<M>
{
  TyEq<Nat_Z, M>? Nat_Visitor<TyEq<Nat_Z, M>?, M>.Visit(TyEq<M, Nat_Z> ty, Nat_Z value)
    => ty.Rot();

  TyEq<Nat_Z, M>? Nat_Visitor<TyEq<Nat_Z, M>?, M>.Visit<X>(TyEq<M, Nat_S<X>> ty, Nat_S<X> value)
    => null;
}

//

interface Nat_S_Mu { }

sealed record Nat_S<N>(N Prev) : Nat<Nat_S<N>>, Hk<Nat_S_Mu, N>
    where N : Nat<N>
{
  public override R Accept<R>(Nat_Visitor<R, Nat_S<N>> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_S<N>>(), this);

  public override Fin<Nat_S<N>>? ToFin(uint value)
    => value == 0 ? Fin.Z<N>() : Prev.ToFin(value - 1)?.S();

  public override TyEq<Nat_S<N>, M>? Equals<M>(Nat<M> other)
    => other.Accept<TyEq<Nat_S<N>, M>?>(new Nat_S_Equals_Visitor<N, M>(Prev));

  public override uint ToUInt() => 1 + Prev.ToUInt();
}

sealed record Nat_S_Equals_Visitor<N, M>(N Prev) : Nat_Visitor<TyEq<Nat_S<N>, M>?, M>
    where N : Nat<N>
    where M : Nat<M>
{
  TyEq<Nat_S<N>, M>? Nat_Visitor<TyEq<Nat_S<N>, M>?, M>.Visit(TyEq<M, Nat_Z> ty, Nat_Z value)
    => null;

  TyEq<Nat_S<N>, M>? Nat_Visitor<TyEq<Nat_S<N>, M>?, M>.Visit<X>(TyEq<M, Nat_S<X>> ty, Nat_S<X> value)
    => Prev.Equals(value.Prev)?.Succ().Compose(ty.Rot());
}

//

interface Nat_Visitor<R, N>
    where N : Nat<N>
{
  R Visit(TyEq<N, Nat_Z> ty, Nat_Z value);

  R Visit<M>(TyEq<N, Nat_S<M>> ty, Nat_S<M> value)
      where M : Nat<M>;
}

// ---

static class Fin
{
  public static Fin<N> ToFin<N>(this uint value, N bound)
    where N : Nat<N>
    => bound.ToFin(value);

  public static Fin<Nat_S<N>> Z<N>()
      where N : Nat<N>
      => new Fin_Z<N>();

  public static Fin<Nat_S<N>> S<N>(this Fin<N> prev)
      where N : Nat<N>
      => new Fin_S<N>(prev);

  public static Fin<N> Narrow<N>(this Hk<Fin_Mu, N> hk)
      where N : Nat<N>
          => (Fin<N>)hk;
}

//

abstract record Fin<N>() : Hk<Fin_Mu, N>
    where N : Nat<N>
{
  public abstract R Accept<R>(Fin_Visitor<R, N> visitor);

  public A Impossible<A>(TyEq<N, Nat_Z> ty)
      => throw new Exception("impossible: Fin<Nat_Z>");
}

interface Fin_Mu { }

//

sealed record Fin_Z<N>() : Fin<Nat_S<N>>
    where N : Nat<N>
{
  public override R Accept<R>(Fin_Visitor<R, Nat_S<N>> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_S<N>>(), this);
}

//

sealed record Fin_S<N>(Fin<N> Prev) : Fin<Nat_S<N>>
    where N : Nat<N>
{
  public override R Accept<R>(Fin_Visitor<R, Nat_S<N>> visitor)
      => visitor.Visit(new TyEq_Refl<Nat_S<N>>(), this);
}

//

interface Fin_Visitor<R, N>
    where N : Nat<N>
{
  R Visit<M>(TyEq<N, Nat_S<M>> ty, Fin_Z<M> value)
      where M : Nat<M>;

  R Visit<M>(TyEq<N, Nat_S<M>> ty, Fin_S<M> value)
      where M : Nat<M>;
}

// ---

static class Vect
{
  public static Vect<A, Nat_Z> Nil<A>()
      => new Vect_Nil<A>();

  public static Vect<A, Nat_S<N>> Cons<A, N>(this Vect<A, N> tail, A head)
      where N : Nat<N>
      => new Vect_Cons<A, N>(head, tail);

  public static A IndexOf<A, N>(this Fin<N> ix, Vect<A, N> vect)
    where N : Nat<N>
    => vect[ix];
}

//

abstract record Vect<A, N>()
    where N : Nat<N>
{
  public abstract A this[Fin<N> ix] { get; }

  public abstract N Length { get; }
}

//

sealed record Vect_Nil<A>() : Vect<A, Nat_Z>
{
  public override A this[Fin<Nat_Z> ix]
    => ix.Impossible<A>(new TyEq_Refl<Nat_Z>());

  public override Nat_Z Length => Nat.Z();
}

//

sealed record Vect_Cons<A, N>(A Head, Vect<A, N> Tail) : Vect<A, Nat_S<N>>
    where N : Nat<N>
{
  public override A this[Fin<Nat_S<N>> ix]
    => ix.Accept(new Vect_Cons_Index_Visitor<A, N>(this));

  public override Nat_S<N> Length => Tail.Length.S();
}

sealed record Vect_Cons_Index_Visitor<A, N>(Vect_Cons<A, N> Cons) : Fin_Visitor<A, Nat_S<N>>
    where N : Nat<N>
{
  public A Visit<M>(TyEq<Nat_S<N>, Nat_S<M>> ty, Fin_Z<M> value) where M : Nat<M>
      => Cons.Head;

  public A Visit<M>(TyEq<Nat_S<N>, Nat_S<M>> ty, Fin_S<M> value) where M : Nat<M>
  {
    var ix = ty.Prev().LiftL<Fin_Mu>().Rot().Cast(value.Prev).Narrow();
    return Cons.Tail[ix];
  }
}

// ---

abstract record TyEq<A, B>()
{
  public abstract B Cast(A a);

  public abstract TyEq<A, C> Compose<C>(TyEq<B, C> ty);

  public abstract TyEq<B, A> Rot();

  public abstract TyEq<Hk<W, A>, Hk<W, B>> LiftL<W>();
}

sealed record TyEq_Refl<A>() : TyEq<A, A>
{
  public override A Cast(A a)
    => a;

  public override TyEq<A, C> Compose<C>(TyEq<A, C> ty)
    => ty;

  public override TyEq<A, A> Rot()
    => this;

  public override TyEq<Hk<W, A>, Hk<W, A>> LiftL<W>()
    => new TyEq_Refl<Hk<W, A>>();
}

sealed record TyEq_Trust<A, B>() : TyEq<A, B>
{
  public override B Cast(A a)
    => (B)(object)a;

  public override TyEq<A, C> Compose<C>(TyEq<B, C> ty)
    => new TyEq_Trust<A, C>();

  public override TyEq<Hk<W, A>, Hk<W, B>> LiftL<W>()
    => new TyEq_Trust<Hk<W, A>, Hk<W, B>>();

  public override TyEq<B, A> Rot()
    => new TyEq_Trust<B, A>();
}

// ---

interface SomeNat_Visitor<R>
{
  R Visit<N>(N nat) where N : Nat<N>;
}

interface SomeNat
{
  R Accept<R>(SomeNat_Visitor<R> visitor);

  public static SomeNat Z() => Nat.Z().Erase();
}

//

static class SomeNat_Helpers
{
  public static SomeNat ToSomeNat(this uint value)
  {
    SomeNat nat = SomeNat.Z();

    for (uint i = 0; i < value; i++)
    {
      nat = nat.S();
    }

    return nat;
  }

  public static SomeNat Erase<N>(this N nat)
    where N : Nat<N>
    => new SomeNat_Wrap<N>(nat);

  public static SomeNat S(this SomeNat nat)
    => nat.Accept(new SomeNat_S_Visitor());
}

sealed record SomeNat_S_Visitor() : SomeNat_Visitor<SomeNat>
{
  SomeNat SomeNat_Visitor<SomeNat>.Visit<N>(N nat) => nat.S().Erase();
}

//

sealed record SomeNat_Wrap<N>(N Nat) : SomeNat
  where N : Nat<N>
{
  public R Accept<R>(SomeNat_Visitor<R> visitor)
    => visitor.Visit<N>(Nat);
}

// ---

public static class Program
{
  public static void Main()
  {
    var xs = Vect.Nil<int>().Cons(2).Cons(1);

    Console.WriteLine(xs[Fin.Z<Nat_S<Nat_Z>>()]);
    Console.WriteLine(xs[Fin.Z<Nat_Z>().S()]);

    Console.WriteLine(0u.ToFin(bound: xs.Length)?.IndexOf(xs));
    Console.WriteLine(1u.ToFin(bound: xs.Length)?.IndexOf(xs));
    Console.WriteLine(2u.ToFin(bound: xs.Length)?.IndexOf(xs).ToString() ?? "null");

    Console.WriteLine(42u.ToSomeNat().Accept(new Example_SomeNat_Visitor()));

    Console.WriteLine(Nat.Z().S().S().S().Erase().Accept(new Example_SomeNat_Visitor()));
  }
}

sealed record Example_SomeNat_Visitor() : SomeNat_Visitor<uint>
{
  uint SomeNat_Visitor<uint>.Visit<N>(N nat) => nat.ToUInt();
}

Nat.java

package example.playground.nat;

import lombok.EqualsAndHashCode;
import lombok.Value;

import java.util.Optional;

abstract class Nat<N extends Nat<N>> implements Hk<Nat.Mu, N> {

  abstract <R> R accept(Visitor<R, N> visitor);

  abstract <M extends Nat<M>> Optional<TyEq<N, M>> eqTo(M m);

  public static <N extends Nat<N>> Nat<N> narrow(Hk<Nat.Mu, N> hk) {
    return (Nat<N>) hk;
  }

  public static Z z() {
    return new Z();
  }

  public static <N extends Nat<N>> S<N> s(N prev) {
    return new S<>(prev);
  }

  interface Mu {}

  interface Visitor<R, N extends Nat<N>> {
    R visit(TyEq<N, Z> nz, Z z);
    <X extends Nat<X>> R visit(TyEq<N, S<X>> ns, S<X> s);
  }

  static <N extends Nat<N>, M extends Nat<M>> TyEq<S<N>, S<M>> succ(TyEq<N, M> teq) {
    // TODO
    return (TyEq<S<N>, S<M>>) (Object) TyEq.refl();
  }

  static <N extends Nat<N>, M extends Nat<M>> TyEq<N, M> prev(TyEq<Nat.S<N>, Nat.S<M>> teq) {
    // TODO
    return (TyEq<N, M>) (Object) TyEq.refl();
  }

  @Value
  @EqualsAndHashCode(callSuper = false)
  static class Z extends Nat<Z> {

    @Override
    <R> R accept(Visitor<R, Z> visitor) {
      return visitor.visit(TyEq.refl(), this);
    }

    @Override
    <M extends Nat<M>> Optional<TyEq<Z, M>> eqTo(M m) {
      return m.accept(new Visitor<Optional<TyEq<Z, M>>, M>() {
        @Override
        public Optional<TyEq<Z, M>> visit(TyEq<M, Z> nz, Z z) {
          return Optional.of(nz.rot());
        }

        @Override
        public <X extends Nat<X>> Optional<TyEq<Z, M>> visit(TyEq<M, S<X>> ns, S<X> s) {
          return Optional.empty();
        }
      });
    }
  }
  @Value
  @EqualsAndHashCode(callSuper = false)
  static class S<N extends Nat<N>> extends Nat<S<N>> {
    N prev;

    @Override
    <R> R accept(Visitor<R, S<N>> visitor) {
      return visitor.visit(TyEq.refl(), this);
    }

    @Override
    <M extends Nat<M>> Optional<TyEq<S<N>, M>> eqTo(M m) {
      return m.accept(new Visitor<Optional<TyEq<S<N>, M>>, M>() {
        @Override
        public Optional<TyEq<S<N>, M>> visit(TyEq<M, Z> nz, Z z) {
          return Optional.empty();
        }

        @Override
        public <X extends Nat<X>> Optional<TyEq<S<N>, M>> visit(TyEq<M, S<X>> ns, S<X> s) {
          return prev.eqTo(s.getPrev()).map(eqNX -> Nat.succ(eqNX).compose(ns.rot()));
        }
      });
    }
  }
}

// ---

abstract class Fin<N extends Nat<N>> implements Hk<Fin.Mu, N> {

  abstract <R> R accept(Visitor<R, N> visitor);

  interface Mu {}

  public static <N extends Nat<N>> Fin<N> narrow(Hk<Fin.Mu, N> hk) {
    return (Fin<N>) hk;
  }

  public static <N extends Nat<N>> Fin<Nat.S<N>> z() {
    return new Z<>();
  }

  public static <N extends Nat<N>> Fin<Nat.S<N>> s(Fin<N> prev) {
    return new S<>(prev);
  }

  @Value
  @EqualsAndHashCode(callSuper = false)
  public static class Z<N extends Nat<N>> extends Fin<Nat.S<N>> {

    @Override
    <R> R accept(Visitor<R, Nat.S<N>> visitor) {
      return visitor.visit(TyEq.refl(), this);
    }
  }

  @Value
  @EqualsAndHashCode(callSuper = false)
  public static class S<N extends Nat<N>> extends Fin<Nat.S<N>> {
    Fin<N> prev;

    @Override
    <R> R accept(Visitor<R, Nat.S<N>> visitor) {
      return visitor.visit(TyEq.refl(), this);
    }
  }

  interface Visitor<R, N extends Nat<N>> {
    <M extends Nat<M>> R visit(TyEq<N, Nat.S<M>> teq, Fin.Z<M> value);
    <M extends Nat<M>> R visit(TyEq<N, Nat.S<M>> teq, Fin.S<M> value);
  }
}

// ---

abstract class Vect<A, N extends Nat<N>> {

  abstract A get(Fin<N> ix);

  public static <A> Vect<A, Nat.Z> nil() {
    return new Nil<>();
  }

  public static <A, N extends Nat<N>> Vect<A, Nat.S<N>> cons(A head, Vect<A, N> tail) {
    return new Cons<>(head, tail);
  }

  @Value
  @EqualsAndHashCode(callSuper = false)
  public static class Nil<A> extends Vect<A, Nat.Z> {
    @Override
    A get(Fin<Nat.Z> ix) {
      throw new RuntimeException("impossible: Fin<Z>");
    }
  }

  @Value
  @EqualsAndHashCode(callSuper = false)
  public static class Cons<A, N extends Nat<N>> extends Vect<A, Nat.S<N>> {
    A head;
    Vect<A, N> tail;

    @Override
    A get(Fin<Nat.S<N>> ix) {
      return ix.accept(new Fin.Visitor<A, Nat.S<N>>() {
        @Override
        public <M extends Nat<M>> A visit(TyEq<Nat.S<N>, Nat.S<M>> teq, Fin.Z<M> value) {
          return head;
        }

        @Override
        public <M extends Nat<M>> A visit(TyEq<Nat.S<N>, Nat.S<M>> teq, Fin.S<M> value) {
          var ix = Nat.prev(teq).<Fin.Mu>liftL().rot().cast(value.getPrev());
          return tail.get(Fin.narrow(ix));
        }
      });
    }
  }
}

// ---

abstract class TyEq<A, B> {

  private TyEq() {}

  public abstract B cast(A a);

  public abstract <C> TyEq<A, C> compose(TyEq<B, C> eqBC);

  public abstract TyEq<B, A> rot();

  public abstract <X> TyEq<Hk<X, A>, Hk<X, B>> liftL();
  public abstract <X> TyEq<Hk<A, X>, Hk<B, X>> liftR();

  static <A> TyEq<A, A> refl() {
    return new Refl<>();
  }

  @Value
  @EqualsAndHashCode(callSuper = false)
  private static class Refl<A> extends TyEq<A, A> {
    @Override
    public A cast(A a) {
      return a;
    }

    @Override
    public <C> TyEq<A, C> compose(TyEq<A, C> eqBC) {
      return eqBC;
    }

    @Override
    public TyEq<A, A> rot() {
      return this;
    }

    @Override
    public <X> TyEq<Hk<X, A>, Hk<X, A>> liftL() {
      return refl();
    }

    @Override
    public <X> TyEq<Hk<A, X>, Hk<A, X>> liftR() {
      return refl();
    }
  }
}

// ---

@SuppressWarnings("unused")
interface Hk<W, A> {}

// ---

public class Program {

  public static void main(String[] args) {
    var xs = Vect.cons(1, Vect.cons(2, Vect.nil()));

    System.out.println(xs.get(Fin.z()));

    System.out.println(xs.get(Fin.s(Fin.z())));
  }
}

Nat.kt

sealed class TyEq<A, B>() {
    abstract fun cast(a: A): B
    abstract fun rot(): TyEq<B, A>

    class Refl<A>() : TyEq<A, A>() {
        override fun cast(a: A): A = a
        override fun rot(): TyEq<A, A> = this
    }
}

sealed interface Expr<T> {

    companion object {
        fun concat(x: Expr<String>, y: Expr<String>): Expr<String>
            = Concat(TyEq.Refl(), x, y)

        fun string(s: String): Expr<String>
            = Str(TyEq.Refl(), s)
    }

    data class Str<T>(
        val ty: TyEq<T, String>,
        val value: String,
    ) : Expr<T>

    data class Concat<T>(
        val ty: TyEq<T, String>,
        val lhs: Expr<String>,
        val rhs: Expr<String>,
    ) : Expr<T>
}

fun <T> eval(e: Expr<T>): T =
    when (e) {
        is Expr.Str -> e.ty.rot().cast(e.value)
        is Expr.Concat -> e.ty.rot().cast(eval(e.lhs) + eval(e.rhs))
    }

sealed class Nat<N : Nat<N>> {

    fun succ(): S<N> = S(this)

    abstract fun <M : Nat<M>> finOf(ix: Nat<M>): Fin<N>?

    object Z : Nat<Z>() {
        override fun <M : Nat<M>> finOf(ix: Nat<M>): Fin<Z>? = null

        override fun toString(): String = "Z"
    }

    data class S<N : Nat<N>>(val prev: Nat<N>) : Nat<S<N>>() {
        override fun <M : Nat<M>> finOf(ix: Nat<M>): Fin<S<N>>? =
            when (ix) {
                Z -> Fin.Z()
                is S<*> ->
                    when (val f = prev.finOf(ix.prev)) {
                        null -> null
                        else -> Fin.S(f)
                    }
            }
    }
}

sealed class SomeNat {

    fun succ(): SomeNat =
        accept(object : Visitor<SomeNat> {
            override fun <N : Nat<N>> visit(nat: Nat<N>): SomeNat = nat.succ().erase()
        })

    abstract fun <R> accept(visitor: Visitor<R>): R

    companion object {
        val Z = Nat.Z.erase()
        fun <N : Nat<N>> Nat<N>.erase(): SomeNat = Wrap(this)
    }

    interface Visitor<R> {
        fun <N : Nat<N>> visit(nat: Nat<N>): R
    }

    private data class Wrap<N : Nat<N>>(val nat: Nat<N>) : SomeNat() {
        override fun <R> accept(visitor: Visitor<R>): R = visitor.visit(nat)

        override fun toString(): String = "SomeNat(${nat})"
    }
}

sealed class Fin<N : Nat<N>> {

    fun succ(): S<N> = S(this)

    data class Z<N : Nat<N>>(val unit: Unit = Unit) : Fin<Nat.S<N>>()
    data class S<N : Nat<N>>(val prev: Fin<N>) : Fin<Nat.S<N>>()
}

abstract class Vect<A, N : Nat<N>> {

    abstract fun get(ix: Fin<N>): A

    abstract val length: N

    data class Nil<A>(val unit: Unit = Unit) : Vect<A, Nat.Z>() {
        override fun get(ix: Fin<Nat.Z>): A =
            when (ix) {
                else -> error("impossible")
            }

        override val length: Nat.Z = Nat.Z
    }

    data class Cons<A, N : Nat<N>>(val head: A, val tail: Vect<A, N>) : Vect<A, Nat.S<N>>() {
        override fun get(ix: Fin<Nat.S<N>>): A =
            when (ix) {
                is Fin.Z -> head
                is Fin.S -> tail.get(ix.prev)
            }

        override val length: Nat.S<N> = tail.length.succ()
    }
}

fun main(args: Array<String>) {
    println(eval(Expr.concat(Expr.string("hi"), Expr.string("world"))))

    println(Nat.Z.succ().succ().succ())
    println(SomeNat.Z.succ().succ())

    val xs = Vect.Cons(1, Vect.Cons(2, Vect.Nil()))
    println("xs=${xs}")
    println("length=${xs.length}")
    println(xs.get(Fin.Z()))
    println(xs.get(Fin.S(Fin.Z())))

    println(Nat.Z.succ().succ().succ().finOf(Nat.Z))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ()))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ().succ()))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ().succ().succ()))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ().succ().succ().succ()))
}