{-# OPTIONS --without-K #-}
module overloading.core where

-- ## Coercions
--
-- The overloading system implemented in this module is based on
-- **coercions**. A coercion is simply a function converting a type into
-- another. In object-oriented parliance, a coercion embodies an *is-a*
-- relationship.  The two types involved in a coercions are called `Source` and
-- `Target` respectively, and the coercion itself is a function `Source →
-- Target`.
--
-- Coercions are implemented as terms of type `Coercion`, which is a record
-- parameterized over the `Source` and `Target` types, with a single field for
-- the actual coercion function.  Of course, the type `Coercion X Y` is
-- isomorphic to `X → Y`, but using a record prevents possible ambiguities when
-- using coercions as implicit parameters, and potentially makes instance
-- resolution faster.
--
-- The typical scenario where coercions are used is when defining a subtype
-- relationships between types.  Although Agda has no built-in support for
-- subtypes, it is possible to achieve a reasonable level of syntactical
-- convenience with the help of some boilerplace code that specifies the
-- subtyping relation explicitly.  See `category.graph.core` for a detailed
-- example.
--
-- This module also contains some functions to help reduce the amount of
-- boilerplate needed for defining all the coercions necessary for a given type.
-- See `coerce-self` and `coerce-parent` below.
--
-- ## Methods
--
-- The strategy employed by this library to implement overloading goes as
-- follows.  Every type (denoted by `Target` in the following) defines a set of
-- "methods" that constitute its interface, and are inherited by every subtype
-- of `Target`.  Methods are divided into 2 groups:
--
-- - **static methods** are functions that take an argument `X` of a type
-- convertible to `Target`. The typical example of a static method is an
-- explicit coercion function, like `∣_∣` below, which returns the "underlying
-- set" of `X`.  Another example of static method is the `total` function for
-- graphs (see `category.graph.core`).
--
-- - **instance methods** are functions that work without requiring an explicit
-- parameter of type `Target`.  A typical example of instance method is
-- composition in a category (`_∘_`): there's no need to pass the category
-- itself when composing two morphisms.  In order to use instance methods, they
-- have to be enabled explicitly for each instance for which they are used.
-- Every type defines a special module (whose name is by convention always
-- `as-target`, where `target` is replaced with the actual lowercase name of
-- type) which allows instance methods to be enabled.  For example, to use the
-- composition operator for morphisms of a category `C`, one can write:
--
--    open as-category C
--
-- The `as-target` module itself behaves like a *static* method, so it can be
-- used to enable instance methods for any superclass of a given instance.
-- Furthermore, enabling instance methods for `Target` enables instance methods
-- for all superclasses of it in its principal inheritance path (see
-- "Inheritance Model" below).
--
-- ## Implementation
--
-- The implementation of static methods is relatively straightforward.  A static
-- method is defined as a function taking a coercion to `Target` as an instance
-- argument, and uses the coercion to convert its argument to the correct type.
--
-- As for instance methods, they are implemented as functions that take a record
-- with the full interface of `Target` (called **instance record** below) as an
-- implicit argument (see "Alternative Notations" below for details), and just
-- return the appropriate field.  This can be accomplished very easily using
-- Agda's module system.
--
-- The `as-target` module, used to enable instance methods, is defined as a
-- static method, and works simply by putting the record above into scope.
--
-- ## Alternative Notations
--
-- Some types have an interface which supports alternative notations.  For
-- example, monoids have a "default" notation (`unit` and `_*_`), and an
-- additive notation (`zero` and `_+_`).
--
-- To implement multiple notations, a `Styled` record is used as the implicit
-- parameter for instance methods.  The `Styled` record is parameterized over a
-- `style` parameter (normally `default`), and contains the interface record as
-- its only field.
--
-- The `Styled` record thus serves two purposes:
--
-- - It prevents ambiguities in the resolution of instance arguments: if an
-- interface record is in scope for reasons unrelated to the overloading system,
-- then it will not be accidentally used as the argument of an instance methods,
-- as it's not wrapped in a `Styled` record.
--
-- - It allows instance methods to specify an alternative style parameter for
-- the record in which the interface record is wrapped.  Thus, multiple
-- `as-target` module can be defined, one per supported style, that put the
-- interface record in scope wrapped in the appropriate `Styled` record.  The
-- `styled` function can be used to wrap an interface record using a given
-- style.
--
-- ## Inheritance Model
--
-- Subtyping relations can form an arbitrary directed graph, with a
-- distinguished spanning forest, whose edges we call *principal*.
--
-- Coercions are defined for every pair of connected nodes in the full graph.
-- Exactly one coercion per pair should be defined, regardless of the number of
-- paths that connect it.  Static methods are inherited automatically through
-- paths in the full DAG, since the existence of a coercion is enough for static
-- methods to propagate.
--
-- The principal subgraph is used for inheritance of instance methods.  Namely,
-- the `as-target` record enables all instance methods for the ancestors of
-- `Target` in the principal subgraph.  This is accomplished by simply
-- re-exporting the `as-target` module for the immediate parent of
-- `Target`. Extra edges coming out of `Target` can optionally be added as well
-- for convenience.

open import level
open import overloading.bundle

record Coercion {i}{j}(Source : Set i)(Target : Set j) : Set (i  j) where
  constructor coercion
  field
    coerce : Source  Target
open Coercion public

data Style : Set where default : Style

record Styled {i}(style : Style)(X : Set i) : Set i where
  field value : X

styled :  {i}{X : Set i}  (s : Style)  X  Styled s X
styled s x = record { value = x }

-- Trivial coercion: any type can be coerced into itself.
coerce-self :  {i} (X : Set i)  Coercion X X
coerce-self {i} _ = record
  { coerce = λ x  x }

-- Transport a coercion to a `Bundle` subtype.  See `overloading.bundle` for
-- more details on bundles.
coerce-parent :  {i j k}
                {X : Set i}
                {Y : Set j}
                c : Coercion X Y 
               {Struct : X  Set k}
               Coercion (Bundle Struct) Y
coerce-parent  c  = record
  { coerce = λ x  coerce c (Bundle.parent x) }

set-is-set :  {i}  Coercion (Set i) (Set i)
set-is-set {i} = coerce-self _

∣_∣ :  {i j}{Source : Set i}  o : Coercion Source (Set j) 
     Source  Set j
∣_∣  c  = coerce c