Translating the lens tutorial to Kitten

lens.ktn

// data Atom = Atom { _element :: String, _point :: Point }
type Atom:
  case mkatom:
    _element as (Text)
    _point as (Point)

// data Point = Point { _x :: Double, _y :: Double }
type Point:
  case mkpoint:
    _x as (Float64)
    _y as (Float64)

// shiftAtomX :: Atom -> Atom
// shiftAtomX (Atom e (Point x y)) = Atom e (Point (x + 1) y)
define shift_atom_x (Atom -> Atom):
  match case mkatom:
    swap -> e;
    match case mkpoint -> x, y:
      e (x + 1) y point atom

// makeLenses ''Atom
Atom #derive_lens

// makeLenses ''Point
Point #derive_lens

define shift_atom_x (Atom -> Atom):
  \(+ 1) { x point } over

// data Molecule = Molecule { _atoms :: [Atom] } deriving (Show)
type Molecule:
  case molecule:
    _atoms as (List<Atom>)

// makeLenses ''Molecule
Molecule #derive_lens

// shiftMoleculeX :: Molecule -> Molecule
// shiftMoleculeX = over (atoms . traverse . point . x) (+ 1)
define shift_molecule_x (Molecule -> Molecule):
  \(+ 1) { x point traverse atoms } over
  // \(+ 1) do (over) { x point traverse atoms }

define atom (-> Atom):
  "C" (1.0 2.0 mkpoint) mkatom

atom { x point } view // 1.0

// This notation isn’t finalized.
type synonym Lens<A, B> (<F<_>> if (Functor<F<_>>) (A, (B -> F<B>) -> F<A>))
type Lens<A, B> (<F<_>> if (Functor<F<_>>) (A, (B -> F<B>) -> F<A>))
type Lens<A, B> (<F<_>> (A, (B -> F<B>) -> F<A>) where (Functor<F<_>>))
type Lens<A, B> <F<_>> (A, (B -> F<B>) -> F<A>) where (Functor<F<_>>)
type Lens<A, B> <F<_>> (A, (B -> F<B>) -> F<A>) where Functor<F<_>>
type Lens<A, B> (<F<_>> (A, (B -> F<B>) -> F<A>) where Functor<F<_>>)

// lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
// lens sa sbt afb s = sbt s <$> afb (sa s)
define lens<A, B> ((A -> B), (B, A -> A) -> Lens<A, B>):
  -> sa, sbt, afb, s;
  s sa call
  afb call
  { s sbt call } map

// point :: Lens' Atom Point
// point = lens _point (\atom newPoint -> atom { _point = newPoint })
define point (-> Lens<Atom, Point>):
  \_point
  // This notation for named field update is not finalized.
  { -> new_point, atom; atom.(new_point -> _point) }
  lens

// point :: Functor f => (Point -> f Point) -> Atom -> f Atom
// point k atom = fmap (\newPoint -> atom { _point = newPoint }) (k (_point atom))
define point<F<_>> (Atom, (Point -> F<Point>) -> F<Atom>) where (Functor<F<_>>):
  -> atom, k;
  atom._point k call
  { -> new_point; atom.(new_point -> .point) } map

// set :: Lens' a b -> b -> a -> a
// set lens b = over lens (\_ -> b)
define set (A, B, Lens<A, B> -> A):
  -> b, lens;
  { drop b } lens over

// Laws:
// view (lens1 . lens2) = (view lens2) . (view lens1)
// over (lens1 . lens2) = (over lens2) . (over lens1)
// { lens2 lens1 } view = \lens1 view \lens2 view
// { lens2 lens1 } over = \lens1 over \lens2 over
// view id = id
// over id = id
// {{} view} = {}
// {{} over} = {}

define ^. <A, B> (A, Lens<A, B> -> B):
  view

atom ^. { x point }

define shift (…):
  -> lens;
  \(+ 1) lens over

{ x point } shift // Atom -> Atom
{ x point traverse atoms } shift // Molecule -> Molecule

define atom_x (-> Lens<Atom, Float64>):
  x point

define molecule_x (-> Traversal<Molecule, Float64>):
  atom_x traverse atoms

\atom_x shift // Atom -> Atom
\molecule_x shift // Molecule -> Molecule

\atom_x set // Float64, Atom -> Atom
\atom_x view // Atom -> Float64

\molecule_x to_list // Molecule -> Float64

// type Traversal' a b = forall f . Applicative f => (b -> f b) -> (a -> f a)
// “Notice that the only difference between a Lens' and a Traversal' is the type class constraint.”
type Traversal<A, B> (<F<_>> (A, (B -> F<B>) -> F<A>) where Applicative<F<_>>)

trait map<F<_>, A, B> (F<A>, (A -> B) -> F<B>)

// Ugly.
trait synonym Functor<F<_>> (<A, B> map<F<_>, A, B>)

trait pure<F<_>, A> (A -> F<A>)
trait <*> <F<_>, A, B> (F<A -> B>, F<A> -> F<B>)

// Fugly ugly.
trait synonym Applicative<F<_>>
  (<A, B> (pure<F<_>, A>, (<*>)<F<_>, A, B>))

// Better.
// Both traits and constraints can be used in a “where” clause.
// A constraint is just a set of traits.
constraint Applicative<F<_>>:
  pure as <A> (A -> F<A>)
  <*> as <A, B> (F<A>, F<A -> B> -> F<B>)
// This is desugared to something like:
type synonym Applicative<F<_>> where (
  pure as <A> (A -> F<A>),
  (<*>) as <A, B> (F<A>, F<A -> B> -> F<B>),
)

// During inference, “where” clauses need to be lifted:
trait zero<T> (-> T)
define abs …:
  dup
  if ((< zero)):
    neg
// “zero” is inferred as zero.<T>
// Because “zero” is a trait, a constraint zero<T> (-> T) is added to the context. (Permissions?)
// That constraint propagates to “<”, “if”, and “neg”.
// The inferred type of “abs” is:
define abs<T> (-> T) where (zero as (-> T))
// There is no zero<T> quantifier in the constraint because it’s the same T from the abs<T> quantifier.
// So could this be encoded with permissions?
// dup                    :: T -> T, T +(clone<T>)
// zero                   :: -> T +(zero<T>)
// (<)                    :: T, T -> Bool +((<)<T>)
// neg                    :: T -> T +(neg<T>)
// if {neg}               :: T, Bool -> T +(neg<T>)
// dup zero               :: T -> T, T, T (clone<T>, zero<T>)
// dup zero (<)           :: T -> T, Bool +((<)<T>, clone<T>, zero<T>)
// dup zero (<) if {neg}  :: T -> T +((<)<T>, clone<T>, neg<T>, zero<T>)
// That type is correct & precise, but cumbersome.
// Some kind of simplification step could prettify type signatures (at least for suggestions).
// E.g. “find the smallest constraint that contains the greatest number of the mentioned traits”.
// (There might be multiple optimal solutions.)
// dup zero (<) if {neg}  :: T -> T +(Compare<T>, Copy<T>, Group<T>)

type Traversal<A, B> (<F<_>> (A, (B -> F<B>) -> F<A>) where Applicative<F<_>>)
type Traversal<A, B> (<F<_>> (A, (B -> F<B>) -> F<A>) where (
  pure<A> (A -> F<A>),
  (<*>) <A, B> (F<A>, F<A -> B> -> F<B>;
)
type Traversal<A, B> (<F<_>> (A, (B -> F<B>) -> F<A>) where (
  pure<A> (A -> F<A>),
  (<*>) <A, B> (F<A>, F<A -> B> -> F<B>;
)