module Stdlib.Trait.Functor.Monomorphic;

import Stdlib.Data.Fixity open;
import Stdlib.Data.Unit open;
import Stdlib.Trait.Functor.Polymorphic as Poly;

{-# specialize: true #-}
trait
type Functor (Container Elem : Type) :=
  mkFunctor@{
    syntax iterator map {init := 0; range := 1};
    {-# specialize: [1] #-}
    map : (Elem -> Elem) -> Container -> Container;
  };

open Functor public;

{-# inline: case #-}
fromPolymorphicFunctor
  {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem :=
  mkFunctor@{
    map := Poly.map;
  };

syntax operator <$> lapp;
{-# inline: true #-}
<$>
  {Container Elem}
  {{Functor Container Elem}}
  (fun : Elem -> Elem)
  (container : Container)
  : Container := map fun container;

syntax operator $> lapp;
{-# inline: true #-}
$>
  {Container Elem : Type}
  {{Functor Container Elem}}
  (container : Container)
  (element : Elem)
  : Container := \{_ := element} <$> container;