self-dependent-types.java

import java.util.function.Function;

// Learning exercise - porting the following ideas:
// https://github.com/moonad/FormCoreJS/blob/master/FormCore.js
// https://github.com/Soonad/Formality-Core/blob/master/Whitepaper.md
// https://github.com/Kindelia/Kind/blob/master/base/Kind/Core.kind
// https://github.com/yatima-inc/yatima-lang-alpha/blob/main/core/src/term.rs

// TODO

class Main {  

  /*

  public abstract class Term {
    public class TypeError extends Exception {}
    public class UnboundReferenceError extends TypeError {}
    
    private Term reduce(Definitions topLevelDefinitions)  {
      return this;
    }

    private normalize(Definitions topLevelDefinitions) throws TypeError;
    
    public static Term typeAnnotation(Term type, Term expression) {
      return new Term() {
        Term reduce(Definitions topLevelDefinitions) {
          return expression.reduce(toopLevelDefinitions);
        }

        Term normalize(Definitions topLevelDefinitions) throws TypeError {
          return
        }
      };
    }

    public static Term typeOfType() {
      return new Term() {
      };
    }

    public static Term selfType(Term body) {
      return new Term() {
      };
    }

    public static Term functionType(Term domain, Term image) {
      return new Term() {
      };
    }

    public static Term functionDefinition(Term body) {
      return new Term() {
      };
    }

    public static Term functionApplication(Term function, Term argument) {
      return new Term() {
        @Override
        public Term reduce(Definitions topLevelDefinitions) {
          // Beta-reduction
          return function.reduce(topLevelDefinitions); // TODO
        }
      };
    }

    public static Term variable(int deBrujinIndex) {
      return new Term() {
      };
    }

    public static Term topLevelReference(String name) {
      return new Term() {
        @Override
        public Term reduce(Definitions topLevelDefinitions) {
          // Dereference
          return topLevelDefinitions.get(name)
            .map(term -> term.reduce(topLevelDefinitions))
            .orElse(this);
        }
      };
    }
  }
  //*/

  /*
  @FunctionalInterface
  public interface Case0<O> {
    O apply();
  }
  @FunctionalInterface
  public interface Case1<I1, O> {
    O apply(I1 i1);
  }
  @FunctionalInterface
  public interface Case2<I1, I2, O> {
    O apply(I1 i1, I2 i2);
  }
  @FunctionalInterface
  public interface Case3<I1, I2, I3, O> {
    O apply(I1 i1, I2 i2, I3 i3);
  }

  interface Term {
    <T> T match(
      Case2<Term, Term, T> typeAnnotation,
      Case0<T> typeOfType,
      Case1<Term, T> selfType,
      Case2<Term, Term, T> functionType,
      Case1<Term, T> functionDefinition,
      Case2<Term, Term, T> functionApplication,
      Case1<Integer, T> variable,
      Case1<String, T> topLevelReference // for mutual recursions
    );

    public static Term typeAnnotation(Term type, Term term) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return typeAnnotation.apply(type, term);
        }
      };
    }

    public static Term typeOfType() {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return typeOfType.apply();
        }
      };
    }

    public static Term selfType(Term body) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return selfType.apply(body);
        }
      };
    }

    public static Term functionType(Term domain, Term image) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return functionType.apply(domain, image);
        }
      };
    }

    public static Term functionDefinition(Term body) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return functionDefinition.apply(body);
        }
      };
    }

    public static Term functionApplication(Term function, Term argument) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return functionApplication.apply(function, argument);
        }
      };
    }

    public static Term variable(int deBrujinIndex) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return variable.apply(deBrujinIndex);
        }
      };
    }

    public static Term topLevelReference(String name) {
      return new Term() {
        @Override
        public <T> T match(
          Case2<Term, Term, T> typeAnnotation,
          Case0<T> typeOfType,
          Case1<Term, T> selfType,
          Case2<Term, Term, T> functionType,
          Case1<Term, T> functionDefinition,
          Case2<Term, Term, T> functionApplication,
          Case1<Integer, T> variable,
          Case1<String, T> topLevelReference
        ) {
          return topLevelReference.apply(name);
        }
      };
    }

    // TODO: Seems very unoptimized. Can we batch these?
    //**
    // * Recurse to the variable leaves and substitute in the value for the variables that came from the specified depth.
    // *
    public static Term betaReduce(Term term, int depth, Term substitution) {
      return term.match(
        (type, expression) -> typeAnnotation(
          betaReduce(type, depth, substitution),
          betaReduce(expression, depth, substitution)
        ),
        () -> term,
        (body) -> selfType(betaReduce(term, depth + 1, substitution)), // Self types introduce a binding, so depth + 1
        (domain, image) -> functionType(
          betaReduce(domain, depth, substitution),
          betaReduce(image, depth, substitution)
        ),
        (body) -> functionDefinition(betaReduce(body, depth + 1, substitution)), // Lambdas introduce a binding, so depth + 1
        (function, argument) -> functionApplication(
          betaReduce(function, depth, substitution),
          betaReduce(argument, depth, substitution)
        ),
        (deBrujinIndex) -> depth == deBrujinIndex ? substitution : term, // Substitute the variable
        (name) -> term
      );
    }

    public static Term reduce(Term term, Definitions topLevelDefinitions) {
      return term.match(
        (type, expression) -> reduce(expression, topLevelDefinitions),
        () -> term,
        (body) -> term,
        (domain, image) -> term,
        (body) -> term,
        (function, argument) -> betaReduce(reduce(function, topLevelDefinitions), 0, argument), // TODO: why don't we reduce the argument?
        (deBrujinIndex) -> term,
        (name) -> topLevelDefinitions.resolve(name).orElse(topLevelReference(name))
      );
    }
    
    public static Term normalize(Term term, Definitions topLevelDefinitions) {
      return reduce(term, topLevelDefinitions)
        .match(
          (type, expression) -> normalize(expression, topLevelDefinitions),
          () -> typeOfType(),
          (body) -> selfType(normalize(body, topLevelDefinitions)),
          (domain, image) -> functionType(
            normalize(domain, topLevelDefinitions),
            normalize(image, topLevelDefinitions)
          ),
          (body) -> functionDefinition(normalize(body, topLevelDefinitions)),
          (function, arguments) -> functionApplication(
            normalize(function, topLevelDefinitions),
            normalize(arguments, topLevelDefinitions)
          ),
          (deBrujinIndex) -> variable(deBrujinIndex),
          (name) -> topLevelReference(name)
        );
    }

    public static class TypeError extends Exception {}
    public static class UnboundReferenceError extends TypeError {}

    public static Term inferType(Term term, Definitions topLevelDefinitions, Context context) throws TypeError {
      return term.match(
        (type, expression) -> ,
        () -> typeOfType(),
        (body) -> {
          return typeOfType();
        },
        (domain, image) -> ,
        (body) -> ,
        (function, argument) -> ,
        (deBrujinIndex) ->,
        (name) -> 
      );
    }

    public static void checkType(Term term, Term type) throws TypeError {
      
    }
  }
  
//return term.match(
//        (type, expression) -> ,
//        () -> ,
//        (body) -> ,
//        (domain, image) -> ,
//        (body) -> ,
//        (function, argument) -> ,
//        (deBrujinIndex) ->,
//        (name) -> 
//      );

  //*/

  
  @FunctionalInterface
  public interface Case0<O> {
    O apply();
  }
  @FunctionalInterface
  public interface Case1<I1, O> {
    O apply(I1 i1);
  }
  @FunctionalInterface
  public interface Case2<I1, I2, O> {
    O apply(I1 i1, I2 i2);
  }
  @FunctionalInterface
  public interface Case3<I1, I2, I3, O> {
    O apply(I1 i1, I2 i2, I3 i3);
  }

  interface Term {
    <T> T match(
      Case2<Term, Term, T> application,
      Case1<Primitive, T> primitive
    );

    interface Primitive {
      <T> T match(
        Case0<T> S,
        Case0<T> S,
        Case0<T> I,
        Case0<T> TypeAnnotation,
      );
    }
  }
  
  public static void main(String args[]) { 
    System.out.println("Hello, world!"); 
  } 
}