Created
November 29, 2017 14:50
-
-
Save U007D/2d91fdbb34599ab125e2c6702df499ac to your computer and use it in GitHub Desktop.
Simulated HKT in Rust via type lenses
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Project the generics out into an HList | |
pub trait Unapply { | |
type Out: ty::Tm<ty::List<ty::Star>> + HList; | |
} | |
// Reapply the type to a fresh set of generics | |
pub trait Reapply<Args: ty::Tm<ty::List<ty::Star>>> | |
: Unapply | |
{ | |
type Out: Unapply<Out = Args>; | |
} | |
// Unapply/Reapply will be automatically derived with #[hkt] | |
// // Path will replace Nat for HKT to support nested substitutions | |
// pub type Path = ty::list::NonEmpty<ty::nat::Nat>; | |
// Types higher-kinded with respect to a location pointed to by a Nat (Path) | |
pub trait HKT<N: ty::Tm<ty::nat::Nat> = ty::_0b> // N is defaulted to 0 (first ty param) | |
: Unapply | |
+ Reapply<<Self as Unapply>::Out, Out = Self> | |
{ | |
// The lens provides a structure to manipulate a particular generic parameter | |
type Lens: ty::Infer<Ty = ty::Lens<ty::List<ty::Star>, ty::Star>>; | |
} | |
// Blanket impl of HKT for all types supporting Unapply/Reapply with a param at N | |
impl<N, Tx> HKT<N> for Tx where | |
N: ty::Tm<ty::nat::Nat>, | |
Tx: Unapply, | |
Tx: Reapply<<Tx as Unapply>::Out, Out = Tx>, | |
{ | |
type Lens = ty::Ap1<ty::zipper::Nth<ty::Star>, N>; | |
} | |
// Get<T<X>> == X (according to nat ptr) | |
pub type Get<This, N = ty::_0b> = | |
<ty::Ap1<ty::lens::View<<This as HKT<N>>::Lens>, | |
<This as Unapply>::Out> | |
as ty::Lower>::Out; | |
// Set<T<X>, Y> == T<Y> (according to nat ptr) | |
pub type Set<This, X, N = ty::_0b> = | |
<This as Reapply<ty::Ap<ty::lens::Set<<This as HKT<N>>::Lens>, | |
HC<ty::Lift<X>, | |
HC<<This as Unapply>::Out, | |
HN>>>>>::Out; | |
// Mappable HKTs | |
pub trait Functor<N: ty::Tm<ty::nat::Nat> = ty::_0b>: HKT<N> { | |
fn fmap<B, F>(self, f: F) -> Set<Self, B, N> where | |
F: Fn(Get<Self, N>) -> B; | |
} | |
// Pointed HKTs | |
pub trait Unital<Tx: HKT<N>, N: ty::Tm<ty::nat::Nat> = ty::_0b> | |
: unify::Eq<Get<Tx, N>> | |
{ | |
fn point(self) -> Tx; | |
} | |
// Joinable HKTs | |
pub trait Multiplicative<N: ty::Tm<ty::nat::Nat> = ty::_0b> | |
: HKT<N> | |
+ unify::Eq<Set<Get<Self, N>, Get<Self, N>, N>> | |
{ | |
fn join(self) -> Get<Self, N>; | |
} | |
// Monads | |
pub trait Monad<N: ty::Tm<ty::nat::Nat> = ty::_0b> | |
: Functor<N> | |
where | |
Get<Self, N>: Unital<Self, N>, | |
Set<Self, Self, N>: Multiplicative, | |
{ | |
fn bind<B, F>(self, f: F) -> Set<Self, B, N> where | |
F: Fn(Get<Self, N>) -> Set<Self, B, N>; | |
} | |
// Option is an HKT | |
impl<T> Unapply for Option<T> { | |
type Out = HC<ty::Lift<T>, HN>; | |
} | |
impl<T0, T1> Reapply<HC<ty::Lift<T1>, HN>> for Option<T0> { | |
type Out = Option<T1>; | |
} | |
// Option is a Functor | |
impl<A> Functor for Option<A> { | |
fn fmap<B, F>(self, f: F) -> Option<B> where | |
F: Fn(A) -> B | |
{ | |
self.map(f) | |
} | |
} | |
// Option has point/return | |
impl<A> Unital<Option<A>> for A { | |
fn point(self) -> Option<A> { | |
Some(self) | |
} | |
} | |
// Option has join | |
impl<A> Multiplicative for Option<Option<A>> { | |
fn join(self) -> Option<A> { | |
match self { | |
None => None, | |
Some(x) => x, | |
} | |
} | |
} | |
// Option is a Monad | |
impl<A> Monad for Option<A> { | |
fn bind<B, F>(self, f: F) -> Option<B> where | |
F: Fn(A) -> Option<B> | |
{ | |
self.fmap(f).join() | |
} | |
} | |
#[cfg(test)] | |
mod test { | |
use super::*; | |
#[test] | |
fn test_monad() { | |
Some(true).fmap(|b| !b) == Some(false); | |
<bool as Unital<Option<_>>>::point(true) == Some(true); | |
Some(Some(true)).join() == Some(true); | |
Some(true).bind(|_| 42u64.point()) == Some(42); | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment