# Works with rslide revision 8
# http://gallium.inria.fr/~pouillar/rslide/rslide
documentclass :beamer, :t, :compress, :red
usepackage    :inputenc, :utf8
usepackage    :xspace

latex '\newcommand{\reFLect}{\textit{%
  re\kern-0.04em F\kern-0.05emL\kern-0.29em\raisebox{0.36ex}{ect}}\xspace}'

words "**OCaml**", "**Haskell**", "**ML**"
words "@Intel@", "@INRIA@"
word "Cxx", :style => VerbatimText.new(:latex => '{\bf C++}', :html => '<b>C++</b>')
word "reFLect", :style => VerbatimText.new(:latex => '\reFLect', :html => '<b><sub>re</sub>FL<sup>ect</sup></b>')
word "α", :regexp => /α/, :style => VerbatimText.new(:latex => "$\\alpha$", :html => 'α')
word "β", :regexp => /β/, :style => VerbatimText.new(:latex => "$\\beta$", :html => 'β')
word "δ", :regexp => /δ/, :style => VerbatimText.new(:latex => "$\\delta$", :html => 'δ')
word "σ", :regexp => /σ/, :style => VerbatimText.new(:latex => "$\\sigma$", :html => 'σ')
word "->", :regexp => /->/, :style => VerbatimText.new(:latex => "$\\rightarrow$", :html => '->'.html_encode!)
word "=>", :regexp => /=>/, :style => VerbatimText.new(:latex => "$\\Rightarrow$", :html => '=>'.html_encode!)
word "_+_", :regexp => /_\+_/, :style => VerbatimText.new(:latex => '\_+\_', :html => '_+_')
word "~~>", :regexp => /~~>/, :style => VerbatimText.new(:latex => "$\\longrightarrow$", :html => '⇝')
word 'antiunif', :style => VerbatimText.new(:latex => "$\\otimes$", :html => 'antiunif')
word "'container", :regexp => (/'container/), :style => VerbatimText.new(:latex => '{\it **container}', :html => '<it>**container</it>')
word "'monad", :regexp => (/'monad/), :style => VerbatimText.new(:latex => '{\it **monad}', :html => '<it>**container</it>')

title "Overloading, searching for alternatives"

author "Nicolas Pouillard"
institute do
  > @@Nicolas.Pouillard@inria.fr@@
end

usetheme      :JuanLesPins
usefonttheme  :serif
beamer_header '\setbeamercolor*{titlelike}{parent=structure}'
at_begin_section do
  slide "Outline" do
    tableofcontents 'sectionstyle=show/shaded',
                    'subsectionstyle=show/shaded/hide'
  end
end
beamer_footline 50, 0

extend do
  module ::Rslide::Tags
    Italic.instance_eval { @regexps.delete_at(1) }
    CodeInline.instance_eval { @regexps.delete_at(1) }
    class CodeMl < Code
    end
    class InlineCodeMl < CodeInline
    end
    class ProtectedText
      def highlight_latex! env, txt
        txt.gsub!(/^(\\#|-|!) (.*)$/) do
          tag, x = $1, $2
          case tag
          when "\\#": "{\\color{blue}\\# }#{x}"
          when "-": "{\\color{green}- }#{x}"
          when "!": "{\\color{red}! }#{x}"
          else x
          end
        end
      end
    end
    class Only < Tag
      include BeamerCmd
      include HtmlProxyTag
      def initialize opts
        super(nil, opts)
      end
      def opts_to_latex env
        opts_to_latex_ env
      end
    end
  end
end

maketitle

html_only do
  paragraph.huge1 "Warning: this presentation has a degraded style compared to the Beamer/PDF version"
end

if false then
  slide "Surcharge, une autre alternative" do
    box "Résumé" do

      >>  La  surcharge  reste aujourd'hui un point sensible du design d'un langage.
      En  effet la question de la surcharge se pose souvent pour des fonctions comme
      l'arithmétique  sur  les  types  de  base,  la  comparaison  et l'affichage de
      valeurs.  Dans  l'optique  d'élargir l'horizon sur de tels systèmes, un dérivé
      extrait  du  langage  reFLect  développé  chez  Intel  sera présenté. C'est un
      système  intéressant  car  plus  léger que les type-classes de Haskell, et qui
      s'intègre  mieux au typage de ML. L'exposé sera plus de la forme d'un tutoriel
      que d'une présentation formelle.
    
    end
  end
end

h1 "Introduction"

slide "Introduction" do
  box "Overloading or not?" do
    * Crucial design choice
    * Hard to avoid for comparison, arithmetic and printing
  end
  box "Some languages already have overloading" do
    * Cxx, well used but too complex and not formalized
    * Haskell, less used but well understood
  end
end

slide "While working for Intel..." do
  box "At Intel they develop their own language, reFLect" do
    * Functional and lazy
    * Circuit modeling and BDDs are deeply integrated
    * A fully reflective language
    * An advanced overloading system
    * An interpreter for that language
  end
  box "At INRIA, we develop for them a compiler" do
    * Based on the OCaml environment
    * Sharing the back-end compilers (starting at lambda-code)
    * Lifting the design a bit
  end
end

slide "The reFLect overloading system", '<+->' do
  * Has evolved from version to version
  * Firstly, features "closed overloading"
  * Provides direct and delegated forms
  * Then provides "open overloading"
  * Finally, recursion trough "open overloading"
end

slide "Today's overloading presentation" do
  box "Extends the ML we know" do
    > Closer to OCaml than reFLect: Call-by-value, modules, signatures...
  end
  box "Takes another path, not chronological" do
    > Starting from "open overloading" and then close it
  end
  box "Syntax adopted, closer to OCaml but:" do
    * Operators are escaped like @_+_@ instead of @( + )@
    * @Int.t@, @List.t@... instead of @int@, @list@...
    * Types and constructors application are like functions:
        @List.t Int.t@, @Cons 1 Nil@...
  end
end

h1 "Basic overloading"

slide "Declaring overloaded symbols" do
  >> One declares it by giving a name and a type:

  code_ml do
    : overload print : IO.output -> α -> unit
      overload _+_ : α -> α -> α
  end
  box "The given type is of any form" do
    * Can be a value (no arrow)
    * As many type variables as you want
    * Type variables are implicitly universally quantified
    * This type scheme is called the anti-unifier
  end
end

slide "Declaring instances" do
  >> One gives the overloaded name and a list of new alternatives.

  code_ml do
    : instance print Int.print Float.print
      instance _+_ Int._+_ Float._+_
  end
  box "Each alternative must be" do
    * Unifiable with the anti-unifier
    * Non-unifiable with all other alternatives
  end
end

slide "Overloading and type inference" do
  > Type inference in this system is a two step process:
  box "Traditional Hindley-Milner type inference", '<2,3>' do
    * Fast, linear (in practice) in the size of the abstract syntax tree
    * Starts with the anti-unifier for occurrences of overloaded symbols
    * Gathers constraints on the type of occurrences
  end
  box "Overload resolution", '<3>' do
    * Searches for a unique most-general satisfying assignment to
      the type variables in those constraints
    * With all the complexity that entails
  end
end

slide "The outcome of overloading (basic)" do
  box "Candidates:" do
    * A candidate is valid when it is unifiable with the constrained occurrence
    * Finally on each occurrence of an overloaded symbol, we have a
      list of valid candidates
  end
  box "The simplified outcome:", '<2>' do
    * When only one candidate: keep it
    * Else: raise an overloading error
  end
end

slide "Simple examples" do
  code_ml do
  : # let isucc x = 1 + x
    - val isucc : Int.t -> Int.t

    # let fsucc x = 1.0 + x
    - val fsucc : Float.t -> Float.t

    # let foo x y = if x = y then x + 12 else y + y
    - val foo : Int.t -> Int.t -> Int.t
  end
end

slide "Simple errors" do
  code_ml do
  : # false + true
    ! Unresolved symbol: _+_ : Bool.t -> Bool.t -> Bool.t
    ! The 2 possible alternatives are:
    !   Int._+_ : Int.t -> Int.t -> Int.t
    !   Float._+_ : Float.t -> Float.t -> Float.t
    
    # fun x -> x + x
    ! Unresolved symbol: _+_ : α -> α -> α
    ! The 2 possible alternatives are:
    !   Int._+_ : Int.t -> Int.t -> Int.t
    !   Float._+_ : Float.t -> Float.t -> Float.t
  end
end

slide "A more complex example" do
  invisible_join do
    only('<1,2>').code_ml do
    : # let id_int x = x + 0
      - val id_int : Int.t -> Int.t
      # let id_bool x = x && true
      - val id_bool : Bool.t -> Bool.t
      # let id_float x = x + 0.0
      - val id_float : Float.t -> Float.t
      # overload id1 : α -> α
      # instance id1 id_int id_bool
      # overload id2 : α -> α
      # instance id2 id_float id_int
      # fun x -> id1 (id2 x)
    end
    only('<2>').inline_code_ml do
    : - <fun> : Int.t -> Int.t
    end
  end
end

slide "Why alternatives must be pairwise not unifiable?" do
  code_ml do
  : # let inc_fst p = fst p + 1
    - val inc_fst : (Int.t * α) -> Int.t
    # let inc_snd p = snd p + 1
    - val inc_snd : (α * Int.t) -> Int.t
    # overload inc_one : (α * β) -> Int.t
    # instance inc_one inc_fst inc_snd
    ! Attempt to overload "inc_one" with alternatives...
    !   inc_fst : (Int.t * α) -> Int.t
    !   inc_snd :: (β * Int.t) -> Int.t
  end
  > Indeed @inc_one(42,true)@ and @inc_one("foo",64)@ make sense, but what about @inc_one(16,64)@?
end

slide "Overloading and modularity" do
  * Better distinction since we must give to the candidate a name
  * And then, add the candidates to an overloaded symbol
  * Modules like @Int@, @Float@ are concrete
  * A module like @Num@ can declare overloaded symbols
  * Then the user can choose and is not a prisoner of overloading
end

h1 "Delegated overloading"

slide "Delegated overloading" do
  box "One wants to compile such a generic definition" do
    code_ml do
    : let double x = x + x
    end
  end
  box "The solution adopted" do
    > An overloading error (too much candidates) becomes an implicit argument when
      the overloading can be resolved later
  end
  box "In a nutshell" do
    > While classic overloading is just some type directed sugar,
      delegated overloading allows generic programming
  end
end

slide "The outcome of overloading (complete)" do
  box "Context" do
    * Are we defining a value? (called @def@)
    * Is this choice "future proof"? (called @future_proof@)
  end
  box("Outcome").code_ml do
  : > *if* no candidates *and* @future_proof@ *then*
    >   raise an overloading error
    > *else* *if* only one candidate
    >     *and* (@future_proof@ *or* *not* @def@) *then* keep it
    > *else* *if* @def@ *then* abstract over its implementation
    > *else* raise an overloading error
  end
end

slide "How delegated overloading works" do
  box "Principle" do
    >> When an overloaded symbol cannot be resolved but could be in the future,
    we abstract the current definition from the implementation of unresolved
    symbols.

    >> These implicit arguments are then re-introduced at each call
    site as overloaded occurrences.

  end
  box "Note" do
    > In this system, the resolution strategy is fixed
  end
end

slide "Delegated overloading in action" do
  code_ml do
    : # let double x = x + x
      - val double : [_+_ : α -> α -> α] => α -> α
  end
  > In fact the definition of @double@ implicitly becomes:
  code_ml do
  : let double' _+_ x = x + x
  end
  > And a call to the function @double@ is treated like that:
  code_ml do
    : double 42
      ~~> double' (_+_ : α -> α -> α) 42
      ~~> double' (_+_ : Int.t -> Int.t -> Int.t) 42
      ~~> double' Int._+_ 42
  end
end

slide "Implicit arguments" do
  box "For each occurrence" do
    > Given an overloaded symbol @f@:
    code_ml do
    : f : [a1 : t1, ..., aN : tN] => t
    end
    > Add all implicit arguments
    code_ml do
    : f x ~~> (f' : t1 -> ... -> tN -> t) a1 ... aN x
    end
  end
  box "Implicit arguments are:" do
    * lexically ordered
    * distinct by name and type (others are merged)
  end
end

slide "Closing the overloading" do
  box "Prevent a symbol from being extended:" do
    * Is useful from development policy point of view
    * Can help the typing algorithm to pick a candidate
  end
  box("Syntax of closing").code_ml do
  : close_overload _+_
  end
  box "@future_proof@ extension" do
    > We extend the @future_proof@ predicate to return true when the
      overloaded symbol is closed
  end
end

slide "Guessing the anti-unifier" do
  > One can provide short-cut for "closed overloading",
    by just taking candidates and computing the least general anti-unifier
  code_ml do
  : t ::= X | F T1...TN

    t         antiunif t         = t
    F t1...tN antiunif F u1...uN = F (t1 antiunif u1)...(tN antiunif uN)
    t         antiunif u         = fresh_var t u
  # forall t1 t2. exist uniq x. x # dom(S) /\ S(t1, t2) = x
  # U = { ((t1, t2), x) | x <-  }
  # fresh_var t1 t2 = assoc (t1, t2) U
  end
end

h1 "Recursion"

slide "Recursive functions" do
  box "A compilation choice" do
    * Choose for once the set of implicit arguments
    * Pass different implicit arguments trough recursive calls
  end
  > The second choice will require an annotation, and will be useful only
    with polymorphic recursion (which also often requires an annotation).
  example.code_ml do
  : # let rec print_list = ... print ... print_list ...
    - val print_list :
    -  [print : IO.output -> α -> unit] =>
    -    IO.output -> List.t α -> unit
  end
end

slide "Recursion Through Open Overloading" do
  box "Can a candidate use its own overloaded symbol?" do
    > Seems evident that that printing a list also rely on printing an element,
      that adding pairs rely on adding it's elements
  end
  only('<1>').example.code_ml do
  : # overload size : α -> Int.t
    # let int_size (_:Int.t) = 1
    - val int_size : Int.t -> Int.t
    # let pair_size (x, y) = size x + size y
    - val pair_size :
    -   [size : α -> Int.t, size : β -> Int.t]
    -   => (α * β) -> Int.t
    # instance size int_size pair_size
  end
  only('<2>').box "Impact on the resolution" do
    > Recursion makes recursive the overloading resolution step,
      since resolution can introduce new implicit arguments
  end
end

slide "Recursions Must Be Well Founded" do
  html_only do
    > This example is particulary badly converted to HTML
    newline
  end
  example.invisible_join do
    inline_code_ml "# let "
    only('<5->').inline_code_ml "**rec** "
    inline_code_ml do
    : list_size = function
      # | []    -> 0
    end
    inline_code_ml "# | x::xs -> size x + "
    only('<1-4>').inline_code_ml do
    : size xs
      - val list_size :
      -   [size : α -> Int.t, size : List.t α -> Int.t]
      -   => List.t α -> Int.t
    end
    only('<5->').inline_code_ml do
    : *list_size* xs
      - val list_size :
      -   [size : α -> Int.t]
      -   => List.t α -> Int.t
    end
    inline_code_ml do
      : # instance size list_size
    end
    only('<1,5>').inline_code_ml do
      : # size
    end
    only('<2>').inline_code_ml do
      : # list_size size size
    end
    only('<3>').inline_code_ml do
      : # list_size size (list_size size size)
    end
    only('<4>').inline_code_ml do
      : # list_size size (list_size size (list_size ...))
    end
    only('<6>').inline_code_ml do
      : # list_size size
    end
    only('<7>').inline_code_ml do
      : # list_size (pair_size size size)
    end
    only('<8>').inline_code_ml do
      : # list_size (pair_size int_size int_size)
    end
    inline_code_ml do
      : #  [(1,2); (3,4)]
    end
  end
end

slide "Polymorphic Recursion" do
  example.code_ml do
  : # type sequence α = Unit | Seq α (sequence (α * α))
    # val seq_size :
    #   [size : α -> Int.t] => sequence α -> Int.t
    # instance size seq_size
    # let seq_size = function
    # | Unit -> 0
    # | Seq x xs -> size x + size xs
    - val seq_size : [size : α -> Int.t]
    -             => sequence α -> Int.t
  end
  # let s = Seq 1 (Seq (2,3) (Seq ((4,5), (6,7)) Unit))
  # printf "size s = %d\n" (size s)
end

h1 "Advanced features"

slide "Explicit overloading" do
  > Minor feature but makes the implicit argument system more complete
  example.code_ml do
  : - val implicit : [size : α -> Int.t]
    -                => List.t α -> Int.t
    # explicit_overloading explicit implicit
    - val explicit : (α -> Int.t) -> List.t α -> Int.t
  end
end

slide "Default Values" do
  > Can be really useful too
  example.code_ml do
  : # let print_default oc _ =
    #   IO.print_string oc "?"
    - val print_default : IO.output -> α -> unit
    # default_overloading print print_default
  end
end

slide "Higher order kinds" do
  > Extending the type system with these kinds makes the system more fine grained
  box "Type algebra becomes" do
    * Type constructors are implicitly sorted, at definition time
    * Type variables are explicitly sorted, just checked
    code_ml do
      : T ::= (X, S) | (A, S) | T T
        
        S ::= * | S -> S
    end
  end
  > No it's not higher order unification since the application is not reduced
end

slide "Higher order kinds, examples" do
  example.code_ml do
  : # overload map :
    #   (α -> β) -> 'container α -> 'container β
    
    # overload bind :
    #   'monad α -> (α -> 'monad β) -> 'monad β
    
    # type view 'container α =
    #    Nil | Cons α ('container α)
    
    # type stateM σ 'monad α =
    #    State (σ -> 'monad (α * σ))
  end
end

h1 "Conclusion"

slide "Conclusion and questions" do
  center.vcenter.huge1.bold "So, ready for overloading?"
end

# h1 "Bonus"

# slide "Future proof details" do
#   * For open overloaded symbols:
#       Future proof if @vars(occurrence_type) ∩ dom(substitution) = ∅@
#   * For closed overloaded symbols: Future proof
#   * Future proof if @vars(implicit argument types) ⊆ vars(definition type)@
# end