Vect.hs

{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language KindSignatures #-}
{-# Language NoImplicitPrelude #-}
{-# Language StandaloneDeriving #-}
{-# Language TypeFamilies #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Vect where

import Prelude (Show)
import GHC.Types (Type)

data Nat where
  Z :: Nat
  S :: Nat -> Nat
  deriving Show

data Vect (n :: Nat) (a :: Type) where
  Nil  :: Vect Z a
  Cons :: a -> Vect n a -> Vect (S n) a

deriving instance Show a => Show (Vect n a)

head :: Vect (S n) a -> a
head (Cons x _) = x

tail :: Vect (S n) a -> Vect n a
tail (Cons _ xs) = xs

type family Add (n :: Nat) (m :: Nat) :: Nat where
  Add Z m = m
  Add (S n) m = S (Add n m)

(++) :: Vect n a -> Vect m a -> Vect (Add n m) a
Nil ++ ys = ys
(Cons x xs) ++ ys = Cons x (xs ++ ys)

data Fin (n :: Nat) where
  FZ :: Fin (S k)
  FS :: Fin k -> Fin (S k)

deriving instance Show (Fin n)

index :: Vect n a -> Fin n -> a
index (Cons x xs) FZ = x
index (Cons x xs) (FS n) = index xs n

Vect.java

import java.util.Optional;
import java.util.function.Supplier;

abstract class Nat<N extends Nat<N>> {

    static Z zero() {
        return new Z();
    }

    static <N extends Nat<N>> S<N> succ(N pred) {
        return new S<>(pred);
    }

    static Optional<Nat> of(Integer n) {
        if (n < 0) {
            return Optional.empty();
        } else if (n == 0) {
            return Optional.of(zero());
        } else {
            return of(n - 1).map(Nat::succ);
        }
    }

    abstract <R> R fold(Z.Fold<R> z, S.Fold<R> s);

    final boolean isZero() {
        return fold(z -> true, (n, next) -> false);
    }

    final Integer toInt() {
        return fold(z -> 0, (n, next) -> 1 + next.get());
    }

    @Override
    public final String toString() {
        return "Nat[" + toInt() + "]";
    }
}
final class Z extends Nat<Z> {

    @Override
    <R> R fold(Fold<R> z, S.Fold<R> s) {
        return z.apply(this);
    }

    interface Fold<R> {
        R apply(Z n);
    }
}
final class S<N extends Nat<N>> extends Nat<S<N>> {

    final private N pred;

    S(N pred) {
        this.pred = pred;
    }

    @Override
    <R> R fold(Z.Fold<R> z, Fold<R> s) {
        return s.apply(this, () -> pred.fold(z, s));
    }

    interface Fold<R> {
        R apply(S<? extends Nat> n, Supplier<R> next);
    }
}

abstract class Fin<N extends Nat> {

    static <N extends Nat<N>> Fin<S<N>> zero() {
        return new FZ<>();
    }

    static <N extends Nat<N>> Fin<S<N>> succ(Fin<N> pred) {
        return new FS<>(pred);
    }

    static <N extends Nat<N>> Optional<Fin<N>> fromNat(Nat n, N ceil) {
        return Optional.empty();
    }

    interface MatchFZ<R> {
        <N extends Nat<N>> R apply(Fin<S<N>> a);
    }

    interface MatchFS<R> {
        <N extends Nat<N>> R apply(Fin<S<N>> a, Fin<N> b);
    }

    abstract <R> R match(MatchFZ<R> fz, MatchFS<R> fs);

    private final static class FZ<N extends Nat<N>> extends Fin<S<N>> {
        @Override
        <R> R match(MatchFZ<R> fz, MatchFS<R> fs) {
            return fz.apply(this);
        }
    }

    private final static class FS<N extends Nat<N>> extends Fin<S<N>> {

        final Fin<N> pred;

        private FS(Fin<N> pred) {
            this.pred = pred;
        }

        @Override
        <R> R match(MatchFZ<R> fz, MatchFS<R> fs) {
            return fs.apply(this, pred);
        }
    }
}

abstract class Vect<Len extends Nat, Elem> {

    static <Elem> Vect<Z, Elem> nil() {
        return new VNil<>();
    }

    static <N extends Nat<N>, Elem> Vect<S<N>, Elem> cons(Elem head, Vect<N, Elem> tail) {
        return new VCons<>(head, tail);
    }

    static <N extends Nat<N>, Elem> Elem head(Vect<S<N>, Elem> xs) {
        return ((VCons<N, Elem>)xs).head;
    }

    static <N extends Nat<N>, Elem> Vect<N, Elem> tail(Vect<S<N>, Elem> xs) {
        return ((VCons<N, Elem>)xs).tail;
    }

    static <N extends Nat<N>, Elem> Elem index(Vect<N, Elem> xs, Fin<N> ix) {
        return ix.match(
            new Fin.MatchFZ<>() {
                @Override
                public <N extends Nat<N>> Elem apply(Fin<S<N>> a) {
                    return ((VCons<N, Elem>)xs).head;
                }
            },
            new Fin.MatchFS<>() {
                @Override
                public <N extends Nat<N>> Elem apply(Fin<S<N>> a, Fin<N> b) {
                    return index(((VCons<N, Elem>)xs).tail, b);
                }
            }
        );
    }

    static <N extends Nat<N>, Elem> Optional<Elem> index(Vect<N, Elem> xs, Nat n) {
        return Fin.fromNat(n, xs.length()).map(ix -> index(xs, ix));
    }

    static <N extends Nat<N>, Elem> Optional<Elem> index(Vect<N, Elem> xs, Integer ix) {
        return Nat.of(ix).flatMap(n -> index(xs, n));
    }

    abstract Len length();

    private final static class VNil<Elem> extends Vect<Z, Elem> {
        @Override
        Z length() {
            return new Z();
        }
    }

    private final static class VCons<N extends Nat<N>, Elem> extends Vect<S<N>, Elem> {

        final Elem head;
        final Vect<N, Elem> tail;

        VCons(Elem head, Vect<N, Elem> tail) {
            this.head = head;
            this.tail = tail;
        }

        @Override
        S<N> length() {
            return new S<>(tail.length());
        }
    }
}

public class Program {

    public static void main(String[] args) {
        Vect<Z, Object> nil = Vect.nil();

        Vect<S<S<Z>>, Integer> ermana = Vect.cons(1, Vect.cons(2, Vect.nil()));

        System.out.println(Vect.index(ermana, 0));

        Fin.fromNat(null, ermana.length()).map(ix -> Vect.index(ermana, ix));

        System.out.println(Vect.head(ermana));

        System.out.println(Vect.index(ermana, Fin.succ(Fin.zero())));

        System.out.println(ermana.length());
    }
}