Chi

Chi is a function code generator and an isomorphism analyzer for fully parametric functions and functions between selected set of built-in and standard types. Chi stands for Curry-Howard Isomorphism.

This program started as a proof-of-concept to see the mechanical nature of the process of deriving function implementations when the types involved serve as logical propositions under the Curry-Howard Isomorphism.

Chi takes in a function signature and generates the function implementation. At the time of this writing, Chi supports Scala, Java, Haskell, Python, and Typescript.

Chi can also check if two functions are isomorphic. See the Isomorphism section for more details on this.

Contents

1. Installation
2. Running
3. More Examples
   • Scala vs Haskell
   • Python
   • Typescript
4. Isomorphisms
5. Assumptions

Installation

The simplest way to install Chi is to download the distribution from the release page.

Running Chi

Chi supports both UI and REPL.

Running the UI

1. Go to the download destination.
2. Run the jar file: $ java -jar chi-<version>.jar

Here's how it currently looks:

demo1_0.4.0.mov

Updated image:

Running the REPL

Running the REPL is similar to running the UI except you need to pass an additional repl argument: $ java -jar chi-<version>.jar repl

Within the REPL, inputs are evaluated when you press enter:

chi> def apply[A, B]: (A => B) => A => B
Detected language: Scala
Generated code:
def apply[A, B]: (A => B) => A => B =
  identity
  
chi> def fst[A, B]: (A, B) => A
Detected language: Scala
Generated code:
def fst[A, B]: (A, B) => A =
  { case (a, b) =>
    a
  }

chi> def const[A, B]: A => (B => A)
Detected language: Scala
Generated code:
def const[A, B]: A => B => A =
  a => b => a

chi> def compose[A, B, C]: (B => C) => (A => B) => A => C
Detected language: Scala
Generated code:
def compose[A, B, C]: (B => C) => (A => B) => A => C =
  f => g => f.compose(g)

chi> def andThen[A, B, C]: (A => B) => (B => C) => A => C
Detected language: Scala
Generated code:
def andThen[A, B, C]: (A => B) => (B => C) => A => C =
  f => g => g.compose(f)

chi> def foo[A, B, C]: (A => C) => (B => C) => Either[A, B] => C
Detected language: Scala
Generated code:
def foo[A, B, C]: (A => C) => (B => C) => Either[A, B] => C =
  f => g => {
    case Left(a) => f(a)
    case Right(b) => g(b)
  }

chi> def foo[A]: Either[A, A] => A
Detected language: Scala
Generated code:
def foo[A]: Either[A, A] => A =
  {
    case Left(a) => a
    case Right(a) => a
  }

chi> def foo[A, B, C]: (A => C) => (B => C) => B => C
Detected language: Scala
Generated code:
def foo[A, B, C]: (A => C) => (B => C) => B => C =
  f => identity

chi> exit
Bye!

More Examples

Scala and Haskell

For the Pure FP enthusiasts, here's Scala vs Haskell:

Note that in the last example above, the extra info like "Detected Language" are gone. Chi provides an option to hide it. Just go to Preferences > Editor and toggle "Show extra output information".

Python examples:

Typescript examples

Named Parameters

Named parameters are also supported:

chi> def identity(a: A): A
def identity(a: A): A =
  a

chi> def andThen[A, B, C](f: A => B, g: B => C): A => C
def andThen[A, B, C](f: A => B, g: B => C): A => C =
  g.compose(f)

Built-in types

Chi also recognize built-in and standard types:

chi> String idString(String s)
Detected language: Java
Generated code:
String idString(String s) {
    return s;
}

chi> def foo(f: String => Int, g: Float => Int): Either[String, Float] => Int
Detected language: Scala
Generated code:
def foo(f: (String => Int), g: (Float => Int)): (Either[String, Float] => Int) =
  {
    case Left(s) => f(s)
    case Right(h) => g(h)
  }

For Java though, you need to use boxed types.

Supported Languages

As mentioned above, Chi supports Scala, Java, Haskell, Python and Typescript. You only need to input the signature and Chi will automatically detect the language used (though it will prioritize Scala syntax)

chi> def disjunctionElimination[A, B, C](f: A => C, g: B => C): Either[A, B] => C
Detected language: Scala
Generated code:
def disjunctionElimination[A, B, C](
    f: A => C,
    g: B => C
): Either[A, B] => C =
  {
    case Left(a) => f(a)
    case Right(b) => g(b)
  }
  
chi> <A, B> B apply(A a, Function<A, B> f)
Detected language: Java
Generated code:
<A, B> B apply(A a, Function<A, B> f) {
    return f.apply(a);
}

chi> <A, B, C> Function<A, C> compose(Function<B, C> f, Function<A, B> g)
Detected language: Java
Generated code:
<A, B, C> Function<A, C> compose(Function<B, C> f, Function<A, B> g) {
    return a -> f.apply(g.apply(a));
}

chi> <A, B, C> BiFunction<A, B, C> foo(Function<A, C> f)
Detected language: Java
Generated code:
<A, B, C> BiFunction<A, B, C> foo(Function<A, C> f) {
    return (a, b) -> {
        return f.apply(a);
    };
}

chi> foo :: Either (a, b) a -> a 
Detected language: Haskell
Generated code: 
foo :: Either (a, b) a -> a
foo e = case e of
    Left (a, b) -> a
    Right a -> a

Isomorphism

To see if two functions are isomorphic with each other, just place the <=> operator between them:

Assumptions

You can also declare assumptions that you can use to construct your proofs: