# 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 => 'C++')
word "reFLect", :style => VerbatimText.new(:latex => '\reFLect', :html => 'reFLect')
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 => '**container')
word "'monad", :regexp => (/'monad/), :style => VerbatimText.new(:latex => '{\it **monad}', :html => '**container')
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
: - : 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