Skip to content

Instantly share code, notes, and snippets.

@clinuxrulz
Last active May 20, 2016 00:04
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save clinuxrulz/fe9c1ffd36fb3524323e48caa846c396 to your computer and use it in GitHub Desktop.
Save clinuxrulz/fe9c1ffd36fb3524323e48caa846c396 to your computer and use it in GitHub Desktop.
Leibnizian equality
package com.sm.fp.data.eq.type;
import com.sm.fp.kinds.__;
class Coerce<A> implements __<Coerce.Mu,A> {
public static class Mu {}
private final A value;
private Coerce(A value) {
this.value = value;
}
public static <A> Coerce<A> narrow(__<Coerce.Mu,A> a) {
return (Coerce<A>)a;
}
public static <A> Coerce<A> coerce(A value) {
return new Coerce<>(value);
}
public A uncoerce() {
return value;
}
}
/*
* To change this license header, choose License Headers in Project Properties.
* To change this template file, choose Tools | Templates
* and open the template in the editor.
*/
package com.sm.fp.data.collections;
import com.sm.fp.data.collections.list.ListWApplicative;
import com.sm.fp.data.collections.list.ListWApply;
import com.sm.fp.data.collections.list.ListWBind;
import com.sm.fp.data.collections.list.ListWFunctor;
import com.sm.fp.data.collections.list.ListWMonad;
import com.sm.fp.data.eq.type.TypeEq;
import fj.data.List;
import com.sm.fp.kinds.__;
/**
*
* @author Clinton
*/
public class ListW<A> implements __<ListW.Mu,A> {
public static class Mu {}
public static <A> ListW<A> narrow(__<ListW.Mu,A> a) {
return ListW.<A>typeEq().coerce(a);
}
private final List<A> list;
private ListW(List<A> list) {
this.list = list;
}
public static <A> ListW<A> wrap(List<A> list) {
return new ListW<>(list);
}
public List<A> unwrap() {
return list;
}
public static final ListWFunctor functor = new ListWFunctor() {};
public static final ListWApply apply = new ListWApply() {};
public static final ListWApplicative applicative = new ListWApplicative() {};
public static final ListWBind bind = new ListWBind() {};
public static final ListWMonad monad = new ListWMonad() {};
public static <A> TypeEq<__<Mu,A>,ListW<A>> typeEq() {
return MyTypeEq.instance();
}
private static class MyTypeEq<A> implements TypeEq<__<Mu,A>,ListW<A>> {
@SuppressWarnings("unchecked")
@Override
public <C> __<C, ListW<A>> subst(__<C, __<ListW.Mu, A>> a) {
return (__)a;
}
private static final MyTypeEq<?> instance = new MyTypeEq<>();
@SuppressWarnings("unchecked")
public static <A> MyTypeEq<A> instance() {
return (MyTypeEq<A>)instance;
}
}
}
package com.sm.fp.data.eq.type;
import com.sm.fp.kinds.__;
class Refl<A> {
public final TypeEq<A,A> refl = new TypeEq<A,A>() {
@Override
public <C> __<C, A> subst(__<C, A> a) {
return a;
}
};
private static final Refl<?> instance = new Refl<>();
@SuppressWarnings("unchecked")
public static <A> Refl<A> instance() {
return (Refl<A>)instance;
}
}
package com.sm.fp.data.eq.type;
import com.sm.fp.kinds.__;
class Symm<P,A,B> implements __<__<__<Symm.Mu,P>,A>,B> {
public static class Mu {}
public static <P,A,B> Symm<P,A,B> narrow(__<__<__<Symm.Mu,P>,A>,B> a) {
return (Symm<P,A,B>)a;
}
private final __<__<P,B>,A> value;
private Symm(__<__<P,B>,A> value) {
this.value = value;
}
public static <P,A,B> Symm<P,A,B> symm(__<__<P,B>,A> value) {
return new Symm<>(value);
}
public __<__<P,B>,A> unSymm() {
return value;
}
}
package com.sm.fp.data.eq.type;
import com.sm.fp.kinds.__;
public interface TypeEq<A,B> extends __<__<TypeEq.Mu,A>,B> {
class Mu {}
static <A,B> TypeEq<A,B> narrow(__<__<TypeEq.Mu,A>,B> a) {
return (TypeEq<A,B>)a;
}
<C> __<C,B> subst(__<C,A> a);
default <C> TypeEq<A,C> trans(TypeEq<B,C> bc) {
return new TypeEq<A,C>() {
@Override
public <C1> __<C1, C> subst(__<C1, A> a) {
return bc.subst(TypeEq.this.subst(a));
}
};
}
static <A> TypeEq<A,A> refl() {
return Refl.<A>instance().refl;
}
default B coerce(A a) {
return Coerce.narrow(subst(Coerce.coerce(a))).uncoerce();
}
default TypeEq<B,A> symm() {
return TypeEq.narrow(Symm.narrow(subst(Symm.symm(TypeEq.<A>refl()))).unSymm());
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment