Skip to content

Commit

Permalink
RankNTypes (9 May 2018)
Browse files Browse the repository at this point in the history
  • Loading branch information
@jmgimeno
jmgimeno committed May 9, 2018
1 parent 9866ed1 commit 797f9f8
Show file tree
Hide file tree
Showing 4 changed files with 3,544 additions and 63 deletions.
63 changes: 31 additions & 32 deletions rankntypes/rankntypes.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="generator" content="pandoc" />
<meta name="author" content="Juan Manuel Gimeno" />
<meta name="author" content="Juan Manuel Gimeno Illa" />
<title>RankNTypes (second step in the path to lenses)</title>
<style type="text/css">code{white-space: pre;}</style>
<style type="text/css">
Expand Down Expand Up @@ -55,9 +55,9 @@
<div class="slide titlepage">
<h1 class="title">RankNTypes (second step in the path to lenses)</h1>
<p class="author">
Juan Manuel Gimeno
Juan Manuel Gimeno Illa
</p>
<p class="date">2 May 2018</p>
<p class="date">9 May 2018</p>
</div>
<div id="index" class="slide section level1">
<h1>Index</h1>
Expand All @@ -71,13 +71,16 @@ <h1>Index</h1>
<div id="language-extensions" class="slide section level1">
<h1>Language extensions</h1>
<ul>
<li><p>Haskell is a <strong>well defined</strong> Language</p>
<li><p>Haskell is defined (althought not formally) in</p>
<ul>
<li><a href="https://www.haskell.org/onlinereport/">Haskell '98 Report</a></li>
<li><a href="https://www.haskell.org/onlinereport/haskell2010/">Haskell 2010 Report</a></li>
</ul></li>
<li><p>But Haskell was meant to be a playground for experimenting with new functional constructs</p></li>
<li><p>So GHC embraced the notion of extensions: opt-in functionality that gives the user even more tools when writing their programs</p></li>
<li><p>So GHC embraced the notion of extensions:</p>
<ul>
<li>opt-in functionality that gives the user even more tools when writing their programs</li>
</ul></li>
<li><p>The extension that we'll need to use for representing lenses is one that allows <strong>higher rank polymorphism</strong>:</p></li>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><span class="ot">{-# LANGUAGE RankNTypes #-}</span></code></pre></div>
Expand All @@ -94,14 +97,14 @@ <h1>Monomorphism</h1>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><span class="ot">intId ::</span> <span class="dt">Integer</span> <span class="ot">-&gt;</span> <span class="dt">Integer</span>
intId x <span class="fu">=</span> x</code></pre></div>
<ul>
<li><code>intId</code> is a fully defined value (a function) od a fully defined type <code>Integer -&gt; Integer</code></li>
<li><code>intId</code> is a fully defined value (a function) of a fully defined type <code>Integer -&gt; Integer</code></li>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><span class="ot">doubleId ::</span> <span class="dt">Double</span> <span class="ot">-&gt;</span> <span class="dt">Double</span>
doubleId x <span class="fu">=</span> x</code></pre></div>
<ul>
<li><p>This is a complete different value of a completely different types</p>
<li><p>This is a complete different value of a completely different type</p>
<ul>
<li>But their definitions are exactly the same?</li>
<li><strong>But their definitions are exactly the same !!????</strong></li>
</ul></li>
</ul>
</div>
Expand All @@ -113,26 +116,24 @@ <h1>Polymorphism</h1>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell">id<span class="ot"> ::</span> a <span class="ot">-&gt;</span> a
id x <span class="fu">=</span> x</code></pre></div>
<ul>
<li><p>The definition is still the same</p></li>
<li><p>This kind of polymorphism is called <strong>parametric polimorphism</strong> (in other languages known as <em>generics</em>)</p></li>
<li><p><strong>Haskell will only allow this if there is indeed a single definition</strong></p>
<li><p>Haskell will only allow this if there is indeed a <strong>single definition</strong></p>
<ul>
<li>You cannot choose the defintion based on its type</li>
</ul></li>
<li><p>It also adds safety through a property called <strong>parametricity</strong>:</p>
<ul>
<li><p>If we pretend there are no loops or exceptions, then the function <strong>fully determined</strong> by its type.</p></li>
<li><p>If we pretend there are no loops or exceptions, then the <code>id</code> function is <strong>fully determined</strong> by its type.</p></li>
<li><p>So, if we see the type <code>a -&gt; a</code> it must be the identity function !!!</p></li>
</ul></li>
</ul>
</div>
<div id="rank-1-polymorphism" class="slide section level1">
<h1>Rank-1 polymorphism</h1>
<ul>
<li><p>Usuelly the cal <code>id</code> <strong>the identity function</strong> but in fact we should think of it as a <strong>whole family of functions</strong></p>
<li><p>Usually we calll <code>id</code> <strong>the identity function</strong> but in fact we should think of it as a <strong>whole family of functions</strong></p>
<ul>
<li><p>we should really say there is a function <strong>for all</strong> types a</p></li>
<li><p>that is, for every type <code>a</code>, there is and identity function called <code>id</code>, which is of type <code>a -&gt; a</code></p></li>
<li>that is, <strong>for all</strong> type <code>a</code>, there is and identity function called <code>id</code>, which is of type <code>a -&gt; a</code></li>
</ul></li>
<li><p>This is the view of the type-checker and by turning the <code>RankNtypes</code> extension we can be explicit about it</p></li>
</ul>
Expand Down Expand Up @@ -160,18 +161,18 @@ <h1>Rank-1 polymorphism</h1>
</ul>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell">print (id (<span class="dv">3</span><span class="ot"> ::</span> <span class="dt">Integer</span>), id <span class="st">&quot;blah&quot;</span>)</code></pre></div>
<ul>
<li><p>Another way to look at it is in terms of <strong>promise and demand</strong></p>
<li><p>Another way to look at it is in terms of <strong>promise</strong> and <strong>demand</strong></p>
<ul>
<li><p>the <strong>type signature</strong> of <code>id</code> <strong>promises</strong> that the definition works <strong>for all types</strong></p></li>
<li><p>when you actually <strong>apply</strong> the function you <strong>demand a certain type</strong></p></li>
<li><p>This interpretation will be very useful when we move to higher-rank polymorphism</p></li>
<li><p>when you actually <strong>apply</strong> the function to a value, you <strong>demand for a certain type</strong></p></li>
</ul></li>
<li><p>This interpretation will be very useful when we move to higher-rank polymorphism</p></li>
</ul>
</div>
<div id="rank-2-and-higher-polymorphism" class="slide section level1">
<h1>Rank-2 and higher polymorphism</h1>
<ul>
<li>Let's us the explicitness of the quantifier in a type alias</li>
<li>Let's use the explicitness of the quantifier in a type alias</li>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><span class="kw">type</span> <span class="dt">IdFunc</span> <span class="fu">=</span> forall a<span class="fu">.</span> a <span class="ot">-&gt;</span> a</code></pre></div>
<ul>
Expand All @@ -184,40 +185,38 @@ <h1>Rank-2 and higher polymorphism</h1>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><span class="ot">someInt ::</span> <span class="dt">IdFunc</span> <span class="ot">-&gt;</span> <span class="dt">Integer</span></code></pre></div>
<ul>
<li><p>Since any value of type <code>IdFunc</code> must be the identity funcion, <code>someInt</code> is a function which expects the identity function as its argument and returns an Integer</p></li>
<li><p>Let's give it some <em>arbitray</em> definition</p></li>
<li><p>Since any value of type <code>IdFunc</code> must be the identity function, <code>someInt</code> is a function which expects the identity function as its argument and returns an Integer</p></li>
<li><p>Let's give it some <em>arbitrary</em> definition</p></li>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell">someInt id&#39; <span class="fu">=</span> id&#39; <span class="dv">3</span></code></pre></div>
</div>
<div id="rank-2-and-higher-polymorphism-1" class="slide section level1">
<h1>Rank-2 and higher polymorphism</h1>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">someInt ::</span> <span class="dt">IdFunc</span> <span class="ot">-&gt;</span> <span class="dt">Integer</span>
someInt id&#39; <span class="fu">=</span> id&#39; <span class="dv">3</span></code></pre></div>
<ul>
<li>Let's give it some <em>arbitrary</em> definition</li>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell">someInt id&#39; <span class="fu">=</span> id&#39; <span class="dv">3</span></code></pre></div>
<ul>
<li><p>This is something new that we didn’t have before !!!!</p>
<li><p>This is <strong>something new</strong> that we didn’t have before !!!!</p>
<ul>
<li><code>someInt</code> has received a function <code>id'</code> about which it knows that it is the fully fledged polymorphic identity function</li>
<li>so <strong>it can instantiate its type variable as it likes</strong>, and it does so.</li>
</ul></li>
<li><p>The someInt function isn’t even polymorphic !!!!</p>
<ul>
<li>rather it expects a polymorphic function as its argument</li>
<li>rather it <strong>demands</strong> a polymorphic function as its argument</li>
</ul></li>
<li><p>Let's expand the definition of <code>IdFunc</code> to make this much clearer:</p></li>
<li><p>Let's expand the type of <code>IdFunc</code> to make this much clearer:</p></li>
</ul>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">someInt ::</span> (forall a<span class="fu">.</span> a <span class="ot">-&gt;</span> a) <span class="ot">-&gt;</span> <span class="dt">Integer</span></code></pre></div>
</div>
<div id="rank-2-and-higher-polymorphism-2" class="slide section level1">
<h1>Rank-2 and higher polymorphism</h1>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">someInt ::</span> (forall a<span class="fu">.</span> a <span class="ot">-&gt;</span> a) <span class="ot">-&gt;</span> <span class="dt">Integer</span></code></pre></div>
<ul>
<li><p>This function is completely <strong>monomorphic</strong> (its type is not quantified)</p></li>
<li><p>When we apply a polymorphic function like <code>id</code> we get to choose which types to instantiate</p></li>
<li><p>The someInt function does not give us such a choice</p>
<li><p>This function is completely <strong>monomorphic</strong> (its type is not quantified)</p>
<ul>
<li><p>In fact it <strong>requires us</strong> to pass a sufficiently polymorphic function to it such that it can make that choice</p></li>
<li><p>When we apply a polymorphic function like <code>id</code> we get to choose which types to instantiate</p></li>
<li><p>The someInt function does not give us such a choice</p></li>
<li><p>In fact it <strong>demands us</strong> to pass a sufficiently polymorphic function to it such that it can make that choice</p></li>
<li><p>When we <strong>apply</strong> it, we need to <strong>give it choice</strong></p></li>
</ul></li>
<li><p>Let's look at it in terms of <strong>promise / demand </strong>:</p>
Expand All @@ -242,7 +241,7 @@ <h1>Rank-2 and higher polymorphism</h1>
<ul>
<li>This function is <strong>rank-3 polymorphic</strong></li>
</ul>
<div class="sourceCode"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><span class="ot">someOtherInt ::</span> ((forall a<span class="fu">.</span> a <span class="ot">-&gt;</span> a) <span class="ot">-&gt;</span> <span class="dt">Integer</span>) <span class="ot">-&gt;</span> <span class="dt">Integer</span></code></pre></div>
<div class="sourceCode"><pre class="sourceCode haskell"><code class="sourceCode haskell"><span class="ot">someOtherInt ::</span> ((forall a<span class="fu">.</span> a <span class="ot">-&gt;</span> a) <span class="ot">-&gt;</span> <span class="dt">Integer</span>) <span class="ot">-&gt;</span> <span class="dt">Integer</span></code></pre></div>
</div>
<div id="rankntypes-and-lenses" class="slide section level1">
<h1>RankNTypes and Lenses</h1>
Expand Down
63 changes: 32 additions & 31 deletions rankntypes/rankntypes.lhs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
% RankNTypes (second step in the path to lenses)
% Juan Manuel Gimeno
% 2 May 2018
% Juan Manuel Gimeno Illa
% 9 May 2018

Index
=====
Expand All @@ -13,14 +13,16 @@ Index
Language extensions
===================

* Haskell is a __well defined__ Language
* Haskell is defined (althought not formally) in

- [Haskell '98 Report](https://www.haskell.org/onlinereport/)
- [Haskell 2010 Report](https://www.haskell.org/onlinereport/haskell2010/)

* But Haskell was meant to be a playground for experimenting with new functional constructs

* So GHC embraced the notion of extensions: opt-in functionality that gives the user even more tools when writing their programs
* So GHC embraced the notion of extensions:

* opt-in functionality that gives the user even more tools when writing their programs

* The extension that we'll need to use for representing lenses is one that allows __higher rank polymorphism__:

Expand All @@ -42,14 +44,14 @@ Monomorphism
> intId :: Integer -> Integer
> intId x = x

* `intId` is a fully defined value (a function) od a fully defined type `Integer -> Integer`
* `intId` is a fully defined value (a function) of a fully defined type `Integer -> Integer`

> doubleId :: Double -> Double
> doubleId x = x

* This is a complete different value of a completely different types
* This is a complete different value of a completely different type

- But their definitions are exactly the same?
- __But their definitions are exactly the same !!????__

Polymorphism
============
Expand All @@ -59,28 +61,24 @@ Polymorphism
> id :: a -> a
> id x = x

* The definition is still the same

* This kind of polymorphism is called __parametric polimorphism__ (in other languages known as _generics_)

* __Haskell will only allow this if there is indeed a single definition__
* Haskell will only allow this if there is indeed a __single definition__

* You cannot choose the defintion based on its type

* It also adds safety through a property called __parametricity__:

* If we pretend there are no loops or exceptions, then the function __fully determined__ by its type.
* If we pretend there are no loops or exceptions, then the `id` function is __fully determined__ by its type.

* So, if we see the type `a -> a` it must be the identity function !!!

Rank-1 polymorphism
===================

* Usuelly the cal `id` __the identity function__ but in fact we should think of it as a __whole family of functions__

* we should really say there is a function __for all__ types a
* Usually we calll `id` __the identity function__ but in fact we should think of it as a __whole family of functions__

* that is, for every type `a`, there is and identity function called `id`, which is of type `a -> a`
* that is, __for all__ type `a`, there is and identity function called `id`, which is of type `a -> a`

* This is the view of the type-checker and by turning the `RankNtypes` extension we can be explicit about it

Expand Down Expand Up @@ -109,18 +107,18 @@ Rank-1 polymorphism
< print (id (3 :: Integer), id "blah")
* Another way to look at it is in terms of __promise and demand__
* Another way to look at it is in terms of __promise__ and __demand__
- the __type signature__ of `id` __promises__ that the definition works __for all types__
- when you actually __apply__ the function you __demand a certain type__
- when you actually __apply__ the function to a value, you __demand for a certain type__
- This interpretation will be very useful when we move to higher-rank polymorphism
* This interpretation will be very useful when we move to higher-rank polymorphism
Rank-2 and higher polymorphism
==============================
* Let's us the explicitness of the quantifier in a type alias
* Let's use the explicitness of the quantifier in a type alias
> type IdFunc = forall a. a -> a
Expand All @@ -135,29 +133,30 @@ id x = x
> someInt :: IdFunc -> Integer
* Since any value of type `IdFunc` must be the identity funcion, `someInt` is a function which expects the identity function as its argument and returns an Integer
* Since any value of type `IdFunc` must be the identity function, `someInt` is a function which expects the identity function as its argument and returns an Integer
* Let's give it some _arbitray_ definition
* Let's give it some _arbitrary_ definition
> someInt id' = id' 3
Rank-2 and higher polymorphism
==============================
* Let's give it some _arbitrary_ definition
> someInt id' = id' 3
```haskell
someInt :: IdFunc -> Integer
someInt id' = id' 3
```
* This is something new that we didn’t have before !!!!
* This is __something new__ that we didn’t have before !!!!
- `someInt` has received a function `id'` about which it knows that it is the fully fledged polymorphic identity function
- so __it can instantiate its type variable as it likes__, and it does so.
* The someInt function isn’t even polymorphic !!!!
- rather it expects a polymorphic function as its argument
- rather it __demands__ a polymorphic function as its argument
* Let's expand the definition of `IdFunc` to make this much clearer:
* Let's expand the type of `IdFunc` to make this much clearer:
```haskell
someInt :: (forall a. a -> a) -> Integer
Expand All @@ -172,11 +171,11 @@ someInt :: (forall a. a -> a) -> Integer
* This function is completely __monomorphic__ (its type is not quantified)
* When we apply a polymorphic function like `id` we get to choose which types to instantiate
- When we apply a polymorphic function like `id` we get to choose which types to instantiate
* The someInt function does not give us such a choice
- The someInt function does not give us such a choice
- In fact it __requires us__ to pass a sufficiently polymorphic function to it such that it can make that choice
- In fact it __demands us__ to pass a sufficiently polymorphic function to it such that it can make that choice
- When we __apply__ it, we need to __give it choice__
Expand All @@ -202,7 +201,9 @@ Rank-2 and higher polymorphism
* This function is __rank-3 polymorphic__
> someOtherInt :: ((forall a. a -> a) -> Integer) -> Integer
```haskell
someOtherInt :: ((forall a. a -> a) -> Integer) -> Integer
```
RankNTypes and Lenses
=====================
Expand Down
Loading

0 comments on commit 797f9f8

Please sign in to comment.