module Stdlib.Trait.Functor.Polymorphic;

import Stdlib.Data.Fixity open;
import Stdlib.Data.Unit open;

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

open Functor public;

syntax operator <$> lapp;
{-# inline: true #-}
<$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f B := map;

syntax operator $> lapp;
{-# inline: true #-}
$> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B :=
  λ {_ := b} <$> fa;

{-# inline: true #-}
void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit :=
  fa $> unit;