Skip to content

Instantly share code, notes, and snippets.

@Garciat
Last active August 2, 2021 16:12
Show Gist options
  • Save Garciat/d9235d76bb6570ac3d26ee5646f42d97 to your computer and use it in GitHub Desktop.
Save Garciat/d9235d76bb6570ac3d26ee5646f42d97 to your computer and use it in GitHub Desktop.
#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();
}
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())));
}
}
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()))
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment