Skip to content

Instantly share code, notes, and snippets.

@Garciat
Last active Nov 12, 2018
Embed
What would you like to do?
{-# 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
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());
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment