Profunctor optics in 1ML --- WORK-IN-PROGRESS!

prelude-extra.1ml

;; -----------------------------------------------------------------------------

;; Unit type
Unit :> {
  type t;
  one : t;
} = {
  type t = bool;
  one = true;
};
unit = Unit.t;

;; -----------------------------------------------------------------------------

;; Function type
type fn a b = a -> b;
flip f y x = f x y;
(|>) (x, f) = f x;

;; -----------------------------------------------------------------------------

;; Product type
type pair a b = (a, b);
cross f g (x, y) = (f x, g y);
fork f g x = (f x, g x);
fst (x, _) = x;
snd (_, y) = y;

;; -----------------------------------------------------------------------------

;; Sum type
inl = left;
inr = right;
either ac bc x = casealt x ac bc;
plus f g = either (f >> inl) (g >> inr);

;; -----------------------------------------------------------------------------

;; Type constructors
type tycon1 = type => type;
type tycon2 = type => type => type;

profunctor-optics.1ml

;; Profunctor optics in 1ML --- WORK-IN-PROGRESS!
;;
;; Background:
;;
;;   https://people.mpi-sws.org/~rossberg/1ml/
;;   http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/poptics.pdf
;;
;; Run as:
;;
;;   ./1ml prelude.1ml prelude-extra.1ml profunctor-optics.1ml

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Basic computation signatures
type FUNCTOR = {
  type t a;
  map 'a 'b: (a -> b) -> t a -> t b;
};

type POINTED = {
  include FUNCTOR;
  pure 'a: a -> t a;
};

type APPLICATIVE = {
  include POINTED;
  apply 'a 'b: t (fn a b) -> t a -> t b;
};

type MONAD = {
  include APPLICATIVE;
  bind 'a 'b: (a -> t b) -> t a -> t b;
};

;; -----------------------------------------------------------------------------

;; Constant functor
Constant (c: type): FUNCTOR = {
  type t a = c;
  map = curry snd;
};

;; Identity monad
Identity: MONAD = {
  type t a = a;
  pure = id;
  map = id;
  apply = id;
  bind = id;
};

;; State monad
State (s: type): MONAD = {
  type t a = s -> (a, s);
  pure = curry id;
  map xy xS = xS >> cross xy id;
  apply xyS xS = xyS >> uncurry (flip map xS);
  bind xyS xS = xS >> uncurry xyS;
};

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Profunctor signatures
type PROFUNCTOR = {
  type t a b;
  dimap 'a 'b 'c 'd: (c -> a) -> (b -> d) -> t a b -> t c d;
};

type CARTESIAN = {
  include PROFUNCTOR;
  first 'a 'b 'c: t a b -> t (pair a c) (pair b c);
  second 'a 'b 'c: t a b -> t (pair c a) (pair c b);
};

type COCARTESIAN = {
  include CARTESIAN;
  left 'a 'b 'c: t a b -> t (alt a c) (alt b c);
  right 'a 'b 'c: t a b -> t (alt c a) (alt c b);
};

type MONOIDAL = {
  include COCARTESIAN;
  par 'a 'b 'c 'd: t a b -> t c d -> t (pair a c) (pair b d);
  empty: t unit unit;
};

;; NOTE that, as a shortcut, `COCARTESIAN` includes `CARTESIAN` and `MONOIDAL`
;; includes `COCARTESIAN`.

;; -----------------------------------------------------------------------------

;; Function profunctor
Fn: MONOIDAL = {
  t = fn;
  dimap f g h = g << h << f;
  first h = cross h id;
  second h = cross id h;
  left h = plus h id;
  right h = plus id h;
  par = cross;
  empty = id;
};

;; UpStar profunctor constructors
UpStar = {
  fromFunctor (F: FUNCTOR): CARTESIAN = {
    type t a b = a -> F.t b;
    dimap f g h = F.map g << h << f;
    local
      rstrength (fx, y) = F.map (fun x => (x, y)) fx;
      lstrength (x, fy) = F.map (fun y => (x, y)) fy;
    in
      first an = rstrength << cross an id;
      second an = lstrength << cross id an;
    end;
  };

  fromPointed (F: POINTED): COCARTESIAN = {
    include fromFunctor F;
    left an = either (F.map inl << an) (F.pure << inr);
    right an = either (F.pure << inl) (F.map inr << an);
  };

  fromApplicative (F: APPLICATIVE): MONOIDAL = {
    include fromPointed F;
    empty = F.pure;
    par h k (x, y) = F.apply (F.apply (F.pure (curry id)) (h x)) (k y);
  };
};

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Optic function types
type   adapter a b s t = (P: PROFUNCTOR)  -> P.t a b -> P.t s t;
type      lens a b s t = (P: CARTESIAN)   -> P.t a b -> P.t s t;
type     prism a b s t = (P: COCARTESIAN) -> P.t a b -> P.t s t; 
type traversal a b s t = (P: MONOIDAL)    -> P.t a b -> P.t s t;

(<~<) (o1:   adapter _ _ _ _, o2:   adapter _ _ _ _) (P: PROFUNCTOR)  = o1 P << o2 P;
(<-<) (o1:      lens _ _ _ _, o2:      lens _ _ _ _) (P: CARTESIAN)   = o1 P << o2 P;
(</<) (o1:     prism _ _ _ _, o2:     prism _ _ _ _) (P: COCARTESIAN) = o1 P << o2 P;
(<*<) (o1: traversal _ _ _ _, o2: traversal _ _ _ _) (P: MONOIDAL)    = o1 P << o2 P;

;; -----------------------------------------------------------------------------

;; A lens
p1 (P: CARTESIAN) = P.dimap (fork fst id) (cross id snd) << P.first;


;; A lens composition
p11 = p1 <-< p1;