<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<base href="x-msg://2548/"><style><!--
/* Font Definitions */
@font-face
        {font-family:Wingdings;
        panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
        {font-family:"MS Mincho";
        panose-1:2 2 6 9 4 2 5 8 3 4;}
@font-face
        {font-family:"MS Mincho";
        panose-1:2 2 6 9 4 2 5 8 3 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
        {font-family:Tahoma;
        panose-1:2 11 6 4 3 5 4 4 2 4;}
@font-face
        {font-family:"\@MS Mincho";
        panose-1:2 2 6 9 4 2 5 8 3 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
p.MsoAcetate, li.MsoAcetate, div.MsoAcetate
        {mso-style-priority:99;
        mso-style-link:"Balloon Text Char";
        margin:0cm;
        margin-bottom:.0001pt;
        font-size:8.0pt;
        font-family:"Tahoma","sans-serif";}
span.apple-converted-space
        {mso-style-name:apple-converted-space;}
span.EmailStyle18
        {mso-style-type:personal-reply;
        font-family:"Calibri","sans-serif";
        color:#1F497D;}
span.BalloonTextChar
        {mso-style-name:"Balloon Text Char";
        mso-style-priority:99;
        mso-style-link:"Balloon Text";
        font-family:"Tahoma","sans-serif";}
.MsoChpDefault
        {mso-style-type:export-only;
        font-size:10.0pt;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
        {page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Brilliant!<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Let my cogs turn….slowly…<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">I think the problem I will have writing these proofs, is how much the compiler “knows” at a given point is not especially clear….you have to build a mental
 model of what its doing.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Interesting stuff though.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<div>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> Richard Eisenberg [mailto:eir@cis.upenn.edu]
<br>
<b>Sent:</b> 13 January 2015 5:13 PM<br>
<b>To:</b> Nicholls, Mark<br>
<b>Cc:</b> haskell-cafe<br>
<b>Subject:</b> Re: [Haskell-cafe] working my way through Data.Type.Equality...my head hurts...<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Hi Mark,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Permit me to take a stab from the beginning.<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">On Jan 13, 2015, at 7:39 AM, "Nicholls, Mark" <<a href="mailto:nicholls.mark@vimn.com">nicholls.mark@vimn.com</a>> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Full code here…</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"><a href="https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs"><span style="color:purple">https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs</span></a></span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">First off, I should point out that Data.Type.Equality, while indeed served at the address above, is now a standard library. The code in that repo is identical to the version that ships with GHC 7.8.<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Lets start at the beginning…</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">data
 a :~: b where</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Refl
 :: a :~: a</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">Looks reasonable….” a :~: b” is inhabited by 1 value…of type “a :~: a”</span><o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">This is true, but there's a bit more going on. If, say, we learn that the type `foo :~: bar` is indeed inhabited by `Refl`, then we know that `foo` and `bar` are the same types. That is<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> baz :: foo :~: bar -> ...<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> baz evidence = case evidence of<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">>   Refl -> -- here, we may assume that `foo` and `bar` are fully identical<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Conversely, whenever we *use* `Refl` in an expression, we must know that the two types being related are indeed equal.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">sym
 :: (a :~: b) -> (b :~: a)</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">sym
 Refl = Refl</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">hmmm… (a :~: b) implies that a is b</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">so (b :~: a)</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">brilliant</span><o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Yes. After pattern-matching on `Refl`, GHC learns that `a` is identical to `b`. Thus, when we use `Refl` on the right-hand side, we know `b` is the same as `a`, and thus the use of `Refl` type checks.<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">--
 | Transitivity of equality</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">trans
 :: (a :~: b) -> (b :~: c) -> (a :~: c)</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">trans
 Refl Refl = Refl</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">--
 | Type-safe cast, using propositional equality</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">castWith
 :: (a :~: b) -> a -> b</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">castWith
 Refl x = x</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">fine….</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">But….</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">--
 | Generalized form of type-safe cast using propositional equality</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">gcastWith
 :: (a :~: b) -> ((a ~ b) => r) -> r</span><o:p></o:p></p>
</div>
<div style="margin-left:36.0pt">
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:-18.0pt"><span style="font-size:11.0pt;font-family:Wingdings;color:#1F497D"></span><span style="font-size:7.0pt;color:#1F497D"> <span class="apple-converted-space"> </span></span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">gcastWith
 Refl x = x</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">I don’t even understand the signature</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going
 on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a”</span><o:p></o:p></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">While the comments I've seen about `~` are quite true, I think there's a simpler way to explain it. `~` is simply equality on types. The constraint `a ~ b` means that `a` is the same type as `b`. We could have
 spelled it `=` if that weren't used elsewhere. Before `~` was added to GHC, it might have been implemented like this:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> class Equals a b | a -> b, b -> a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> instance Equals x x<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> -- no other instances!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The proper `~` works better in type inference than this functional-dependency approach, but perhaps rewriting `~` in terms of functional dependencies is illuminating.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">When a constraint `a ~ b` is in the context, then GHC assumes the types are the same, and freely rewrites one to the other.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The type `(a ~ b) => r` above is a higher-rank type, which is why it may look strange to you. Let's skip the precise definition of "higher-rank" for now. In practical terms: let's say you write `gcastWith proof
 x` in your program. By the type signature of `gcastWith`, GHC knows that `proof` must have type `a :~: b` for some `a` and `b`. It further knows that `x` has the type `(a ~ b) => r`, for some `r`, but the same `a` and `b`. Of course, if a Haskell expression
 as a type `constraint => stuff`, then GHC can assume `constraint` when type-checking the expression. The same holds here: GHC assumes `a ~ b` (that is, `a` and `b` are identical) when type-checking the expression `x`. Perhaps, somewhere deep inside `x`, you
 pass a variable of type `a` to a function expecting a `b` -- that's just fine, because `a` and `b` are the same.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">The `r` type variable in the type of `gcastWith` is the type of the result. It's the type you would naively give to `x`, but without a particular assumption that `a` and `b` are the same.<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><br>
<br>
<o:p></o:p></p>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1F497D">What would a value of type “((a ~ b) => r)” look like?</span><o:p></o:p></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">It looks just like a value of type `r`. Except that GHC has an extra assumption during type-checking. Contrast this to, say,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> min :: Ord a => a -> a -> a<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">> min = \x y -> if x < y then x else y<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">What does a value of `Ord a => a -> a -> a` look like? Identically to a value of type `a -> a -> a`, except with an extra assumption. This is just like the type `(a ~ b) => r`, just less exotic-looking.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt">As for singleton types and dependent types: they're great fun, but I don't think you need to go anywhere near there to understand this module. (Other modules in that repo, on the other hand, get scarier...)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">I hope this helps!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Richard<o:p></o:p></p>
</div>
</div>
<P></P>
<P><br><br>CONFIDENTIALITY NOTICE<br><br>This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.<br><br>While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.<br><br>Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.<br><br>MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe.  MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.<br></P></body>
</html>