Skip to content

Instantly share code, notes, and snippets.

@jorpic

jorpic/index.html

Last active March 27, 2016 09:43
Show Gist options
  • Save jorpic/924c48aa888fc0870f38 to your computer and use it in GitHub Desktop.
Save jorpic/924c48aa888fc0870f38 to your computer and use it in GitHub Desktop.
Download ZIP
Haskell Meetup 2015-12-06
Raw
index.html
<!doctype html>
<html>
<head>
<meta charset="utf-8">
<link href='https://fonts.googleapis.com/css?family=Raleway:500' rel='stylesheet' type='text/css'>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.0.0/styles/github.min.css">
<script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.0.0/highlight.min.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.0.0/languages/haskell.min.js"></script>
<style>
@page {
size: landscape;
}
body {
font-family: sans-serif;
font-size: 4vh;
}
section {
display: flex;
flex-direction: column;
align-items: center;
justify-content: center;
height: 80vh;
padding: 10vh 0 10vh 0;
page-break-after: always;
}
pre {
width: min-content;
width: -moz-min-content;
width: -webkit-min-content;
line-height: 140%;
}
img {
display: block;
height: 60vh;
width: auto;
}
li {
margin-bottom: 0.7em;
}
.email {
font-size: 80%;
opacity: 0.8;
}
.logo {
font-family: 'Raleway', sans-serif;
font-size: 8vh;
color: #333;
opacity: 0.8;
}
.logo .flipA {
display: inline-block;
-moz-transform: scale(1, -1);
-webkit-transform: scale(1, -1);
transform: scale(1, -1);
color: #48045a;
}
.logo .flipE {
display: inline-block;
-moz-transform: scale(-1, 1);
-webkit-transform: scale(-1, 1);
transform: scale(-1, 1);
color: #48045a;
}
#arrow-table th,
#arrow-table td {
text-align: center;
padding: 0.2em 1em 0.2em 1em;
}
pre code.error {
background: pink;
}
</style>
</head>
<body spellcheck=false>
<section id="start">
<h1>Зависимые типы в GHC 8</h1>
<p>Максим Талдыкин</p>
<p class="email">[email protected]</p>
</section>
<section id="what">
<h1>Что такое?</h1>
</section>
<section id="what/sorts">
<pre><code class="haskell">
Just 1 : Maybe Int : * : □
Maybe : * -> * : □
Vec Int Z : * : □
Vec : * -> Nat -> * : □
</code></pre>
</section>
<section id="what/arrows">
<pre><code class="haskell">
map : forall a b. (a -> b) -> [a] -> [b]
map f (x:xs) = f x : map f xs
map f [] = []
</code></pre>
</section>
<section id="what/core">
<pre><code class="haskell">
map :: forall a b. (a -> b) -> [a] -> [b]
map =
\ (@a)
(@b)
(f :: a -> b)
(ds :: [a]) ->
case ds of
[] -> GHC.Types.[] @b
: x xs ->
GHC.Types.: @b (f x) (map @a @b f xs)
</code></pre>
</section>
<section id="what/forall">
<pre><code class="haskell">
forall
(a :: *)
(b :: *)
(f :: a -> b)
(xs :: [a])
. [b]
</code></pre>
</section>
<section id="what/pi">
<pre><code class="haskell">
replicate :: pi (n : Nat) -> a -> Vec a n
replicate Z _ = Nil
replicate (S m) x = x :> replicate m a
</code></pre>
</section>
<section id="what/table">
<table id="arrow-table">
<tr><th> </th><th>vis</th><th>dep</th><th>rel</th></tr>
<tr><td>forall (a : *). a </td><td> - </td><td> + </td><td> - </td></tr>
<tr><td>a -> a </td><td> + </td><td> - </td><td> + </td></tr>
<tr><td>Monad m => m a </td><td> - </td><td> - </td><td> + </td></tr>
<tr><td>pi (a : Bool). f a </td><td> - </td><td> + </td><td> + </td></tr>
<tr><td>pi (a : Bool) -> f a</td><td> + </td><td> + </td><td> + </td></tr>
</table>
</section>
<section id="what/star-in-star">
<h1>* : *</h1>
<h1>pi</h1>
</section>
<section id="why">
<h1>Зачем?</h1>
</section>
<section id="why/good-bad">
<h1>zipWithN, mapT</h1>
<h1>tail []</h1>
</section>
<section id="why/strncpy">
<pre><code class="haskell">
strncpy
:: forall (p q :: Nat)
=> (LE n p ~ True, LE n q ~ True)
. pi (n :: Nat)
-> Ptr Char p
-> Ptr Char q
-> IO ()
</code></pre>
</section>
<section id="why/examples">
<ul>
<li>
<a href="http://www.staff.science.uu.nl/~swier004/Publications/piware.pdf">Π-Ware: Hardware Description</a>
<ul><li>Swierstra et al., 2015</li></ul>
</li>
<li>
<a href="https://eb.host.cs.st-andrews.ac.uk/writings/fi-cbc.pdf">Correct-by-Construction Concurrency</a>
<ul><li>Brady &amp; Hammond, 2009</li></ul>
</li>
<li>
<a href="http://www.cs.cmu.edu/~jamiemmt/papers/ml10sectyp.pdf">Security-Typed Programming</a>
<ul><li>Morgenstern &amp; Licata, 2010 </li></ul>
</li>
</ul>
</section>
<section id="tf">
<h1>Type Families</h1>
</section>
<section id="tf/nat">
<pre><code class="haskell">
data Nat = Z | S Nat
type family
(m :: Nat) :+ (n :: Nat) :: Nat
where
Z :+ n = n
(S k) :+ n = S (k :+ n)
-- Vec a m -> Vec a n -> Vec a (m :+ n)
</code></pre>
</section>
<section id="gadt">
<h1>GADTs</h1>
Generalized Algebraic Data Types
</section>
<section id="gadt/vec">
<pre><code class="haskell">
data Vec :: Nat -> * -> *
Nil :: Vec Z a
(:>) :: a -> Vec n a -> Vec (S n) a
</code></pre>
</section>
<section id="gadt/vec-eq">
<pre><code class="haskell">
data Vec (n :: Nat) (a :: *) :: * where
Nil :: n ~ Z => Nil n a
(:>) :: forall (m :: Nat)
. n ~ S m
=> a -> Vec m a -> Vec n a
</code></pre>
</section>
<section id="gadt/vec-pm">
<pre><code class="haskell">
tail :: Vec (S k) a -> Vec k a
tail (_ :> xs) = xs
-- (m :: Nat) (S k ~ S m)
</code></pre>
</section>
<section id="gadt/vec-concat">
<pre><code class="haskell">
type family
(v :: Vec a m) :++ (w :: Vec a n) :: Vec a k
where
Nil :++ w = w
(x :> xs) :++ w = x :> (xs :++ w)
</code></pre>
</section>
<section id="gadt/vec-concat-error">
<pre><code class="haskell">
type family
(v :: Vec a m) :++ (w :: Vec a n) :: Vec a k
where
Nil :++ w = w
(x :> xs) :++ w = x :> (xs :++ w)
</code></pre>
<pre><code class="error">
‘Vec’ of kind ‘* -> Nat -> *’ is not promotable
In the kind ‘Vec a m’
</code></pre>
</section>
<section id="gadt/vec-kind">
<pre><code class="haskell">
Vec :: □ -> □ -> □
</code></pre>
</section>
<section id="sing/replicate-pi">
<pre><code class="haskell">
replicate :: pi (n :: Nat) -> a -> Vec a n
replicate Z a = Nil
replicate (S m) a = a :> replicate m a
</code></pre>
</section>
<section id="sing/nat">
<pre><code class="haskell">
data Nat = Z | S Nat
data Nat's :: Nat -> * where
Z's :: Nat's Z
S's :: Nat's n -> Nat's (S n)
-- S's Z's :: Nat's (S Z)
</code></pre>
</section>
<section id="sing/replicate-sing">
<pre><code class="haskell">
replicate :: Nat's n -> a -> Vec a n
replicate Z's a = Nil
replicate (S's m) a = a :> replicate m a
</code></pre>
</section>
<section id="suddenly">
<h1>Они уже здесь!</h1>
</section>
<section id="singletons">
<h1>Singleton types here</h1>
<h1>Singleton types there</h1>
<h1>Singleton types everywhere</h1>
<p>Monnier & Haguenauer, 2009</p>
</section>
<section id="hasochism">
<h1>Hasochism</h1>
<p>Lindley & mcBride, 2013</p>
</section>
<section id="gadt/fin">
<pre><code class="haskell">
data Fin :: Nat -> * where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)
</code></pre>
</section>
<section id="gadt/lookup-pi">
<pre><code class="haskell">
lookup :: pi (f :: Fin n) -> Vec a n -> a
lookup FZ (x :> _) = x
lookup (FS i) (_ :> xs) = lookup i xs
</code></pre>
</section>
<section id="gadt/fin-sing">
<pre><code class="haskell">
data Fin's (n :: Nat) (f :: Fin n) :: * where
FZ's :: Fin's (S m) FZ
FS's :: Fin's m g -> Fin's (S m) (FS g)
-- FS's FZ's :: Fin's 4 (FS FZ :: Fin 4)
</code></pre>
</section>
<section id="gadt/fin-sing-error">
<pre><code class="haskell">
data Fin's (n :: Nat) (f :: Fin n) :: * where
FZ's :: Fin's (S m) FZ
FS's :: Fin's m g -> Fin's (S m) (FS g)
</code></pre>
<pre><code class="error">
Kind variable also used as type variable: ‘n’
In the data type declaration for ‘Fin's’
</code></pre>
</section>
<section id="servant">
<pre><code class="haskell">
get "/Contract/:id" $ do
intParam "id" >>= queryDb "Contract" >>= json
type API
= "Contract"
:> Capture "id" Int
:> Get '[JSON] Contract
</code></pre>
</section>
<section id="servant/svc">
<pre><code class="haskell">
type Api
= "Contract"
:> Capture "id" Int
:> RoleFilter "Contract" "owner" '[43, 265]
:> Get '[JSON] (Obj Contract)
</code></pre>
</section>
<section id="servant/data-model">
<pre><code class="haskell">
data User (fieldName :: Symbol) where
Id :: Int -> User "id"
Name :: Text -> User "name"
Roles :: [Vector (Ref Role)] -> User "roles"
data Contract (fieldName :: Symbol) where
Id :: Int -> Contract "id"
Owner :: Ref Role -> Contract "owner"
type family TableName (m :: Symbol -> *) :: Symbol
type instance TableName User = "User"
type instance TableName Contract = "Contract"
</code></pre>
</section>
<section id="servant/svc-dsl">
<pre><code class="haskell">
type Api
= "Contract"
:> Capture "id" Int
:> RoleFilter "Contract" "owner" '[43, 265]
:> Get '[JSON] (Obj Contract)
type Api
= MkFilter Contract
(RoleFilter C.Owner '[Role1, Role2])
</code></pre>
</section>
<section id="servant/svc-dsl-fn">
<pre><code class="haskell">
type family MkFilter
(f :: Symbol)
(m :: Symbol -> *)
(filter :: *)
where
MkFilter f m (RoleFilter (own :: m g) rs)
= TableName m
:> Capture
(FieldName (TableId m))
(FieldType (TableId m))
:> RoleFilter' (TableName m) g rs
:> Get '[JSON] (Obj m)
</code></pre>
</section>
<section id="hard">
<h1>Termination</h1>
<h1>Equality</h1>
<h1>Consistency</h1>
</section>
<section id="theory/refs">
<ul>
<li>
<a href="https://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds.pdf">System FC with Explicit Kind Equality</a>, 2013
</li>
<li>
<a
href="https://github.com/goldfirere/thesis/blob/master/built/proposal.pdf">Dependent Types in Haskell</a>, draft
</li>
<li>
<a href="http://adam.gundry.co.uk/pub/thesis/">Type Inference, Haskell
and Dependent Types</a>, 2013
</li>
</ul>
</section>
<section id="steph">
<img src="http://www.cis.upenn.edu/~sweirich/images/steph-2012.jpg"/>
<p>Stephanie Weirich<p>
</section>
<section id="rae">
<img src="https://www.cis.upenn.edu/~eir/rae.jpg"/>
<p>Richard A. Eisenberg<p>
</section>
<section id="martin">
<img src="http://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/Per_Martin-Lof_big.jpg"/>
<p>Per Martin-Löf, <a href="http://www.csie.ntu.edu.tw/~b94087/ITT.pdf">Intuitionistic type theory (1984)</a></p>
</section>
<section id="theend">
<div class="logo">
<span>F</span>
<span>O</span>
<span>R</span>
<span>M</span>
<span class="flipA">A</span>
<span>L</span>
<span>&nbsp;</span>
<span>M</span>
<span class="flipE">E</span>
<span>T</span>
<span>H</span>
<span>O</span>
<span>D</span>
<span>S</span>
</div>
</section>
<script>
var edit = false;
var sections = [].slice.call(document.getElementsByTagName('section'));
sections.forEach(function(s) {
s.onclick = function() { edit = s.contentEditable = true; };
s.onblur = function() { edit = s.contentEditable = false; };
});
var dict = {};
var root = {prev: null};
var current = root;
sections.forEach(function(s) {
current.hash = '#' + s.id;
current.elem = s;
dict[current.hash] = current;
current = current.next = {prev: current};
});
current.prev.next = null;
function hashchange() {
current = dict[window.location.hash] || root;
}
window.addEventListener('hashchange', hashchange, false);
hashchange();
function keydown(e) {
switch(e.keyCode) {
case 27: /* Esc */
edit = current.elem.contentEditable = false;
break;
case 37: /* Left */ break;
case 38: /* Up */
if(!edit && current.prev) {
window.location.hash = current.prev.hash;
e.preventDefault();
}
break;
case 39: /* Right */ break;
case 40: /* Down */
if(!edit && current.next) {
window.location.hash = current.next.hash;
e.preventDefault();
}
break;
}
}
window.addEventListener('keydown', keydown, false);
hljs.initHighlighting();
</script>
</body>
</html>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment