<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Garamond;
panose-1:2 11 6 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p class="MsoNormal">There’s the singletons library for GHC, and some follow-on work for Dependent Haskell. As far as I can tell it is another one of those drawn-out projects that the Haskell community manages to endure/ignore.
<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black">Friam <friam-bounces@redfish.com> on behalf of Jon Zingale <jonzingale@gmail.com><br>
<b>Reply-To: </b>The Friday Morning Applied Complexity Coffee Group <friam@redfish.com><br>
<b>Date: </b>Friday, March 27, 2020 at 9:46 AM<br>
<b>To: </b>"friam@redfish.com" <friam@redfish.com><br>
<b>Subject: </b>Re: [FRIAM] talk about rabbit holes ...<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">Glen,<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">It is kind of funny to me, and yet should not surprise me, that an<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">individual was motivated to write a theorem prover in R. OTOH,<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">every attempt I have ever made to get Agda to work for me has<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">required sandboxing my Haskell environments and switching to<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">an emacs editor, so hey. Still, the project strikes me as being one<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">of bull headedness, a just-to-see-if-one-can kind of thing.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">Do you think they will go so far as to implement general dependent<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">typing? Last night at some point, I was thinking about the problem of<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">implementing flexible contravariant functors in a computing language.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">This often appears to a stumbling block when I set out to define <i>for all</i><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">and
<i>there exists</i> from a substitution functor, a la Topos theory.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">Any thoughts are welcome.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Garamond",serif;color:#333333">Jon<o:p></o:p></span></p>
</div>
</div>
</div>
</body>
</html>