<html xmlns:v="urn:schemas-microsoft-com:vml" 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=us-ascii">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@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;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-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.BalloonTextChar
{mso-style-name:"Balloon Text Char";
mso-style-priority:99;
mso-style-link:"Balloon Text";
font-family:"Tahoma","sans-serif";}
span.EmailStyle19
{mso-style-type:personal;
font-family:"Calibri","sans-serif";
color:windowtext;}
span.EmailStyle20
{mso-style-type:personal-reply;
font-family:"Calibri","sans-serif";
color:#1F497D;}
.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-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="color:#1F497D">Can someone check my answer (no I’m not doing an assessment…I’m actually learning stuff out of interest!)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB">working through <o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-GB"><a href="https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell">https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell</a><o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">still there is a section about singleton types and the exercise is<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">“Exercise: Define the binary tree type and implement its singleton type.”<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Ok, I think I’m probably wrong….a binary tree is something like…<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">> data BTree a = Leaf | Branch a (BTree a) (BTree a)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">With DataKind<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">My logic goes…<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Leaf is an uninhabited type, so I need a value isomorphic to it….<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Easy?<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">> data SBTree a where<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">> SLeaf :: SBTree Leaf<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Things like <o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Branch Integer Leaf (Branch String Leaf Leaf)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Are uninhabited…so I need to add<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">> SBranch :: (a :: *) -> (SBTree (b :: BTree *)) -> (SBTree (c :: BTree *)) -> SBTree (Branch a b c)<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">?<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">It compiles…but….is it actually correct?<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Things like <o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">> y = SBranch (SS (SS SZ)) SLeaf SLeaf<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">> z = SBranch (SS (SS SZ)) (SBranch SZ SLeaf SLeaf) SLeaf<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:#1F497D">Seem to make sense ish. <o:p></o:p></span></p>
<p class="MsoNormal"><span style="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 style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> Nicholls, Mark
<br>
<b>Sent:</b> 28 April 2015 9:33 AM<br>
<b>To:</b> Nicholls, Mark<br>
<b>Subject:</b> sds<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">Hello,<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">working through
<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><a href="https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell">https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell</a><o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">but a bit stuck...with an error...<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances, GADTs, StandaloneDeriving #-}<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> data Nat = Z | S Nat<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> data Vector a n where<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> Nil :: Vector a Z<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> (:-) :: a -> Vector a n -> Vector a (S n)<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> infixr 5 :-<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">I assume init...is a bit like tail but take n - 1 elements from the front....but...<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> init' :: Vector a ('S n) -> Vector a n<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> init' (x :- Nil) = Nil<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> init' (x :- xs@(_ :- _)) = x :- (init' xs)
<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> zipWithSame f Nil Nil = Nil<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB">> zipWithSame f (x :- xs) (y :- xs@(_ :- _)) = Nil<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><b><span lang="EN-GB" style="font-size:8.0pt;font-family:"Tahoma","sans-serif";color:teal">Mark Nicholls
</span></b><span lang="EN-GB" style="font-size:8.0pt;font-family:"Tahoma","sans-serif";color:teal">| Senior Technical Director, Programmes & Development - Viacom International Media Networks</span><span lang="EN-GB" style="font-size:8.0pt;color:#1F497D"><br>
</span><b><span lang="EN-GB" style="font-size:8.0pt;font-family:"Tahoma","sans-serif";color:teal">A:</span></b><span lang="EN-GB" style="font-size:8.0pt;color:#1F497D">
</span><span lang="EN-GB" style="font-size:8.0pt;font-family:"Tahoma","sans-serif";color:teal">17-29 Hawley Crescent London NW1 8TT |
<b>e:</b> <a href="mailto:mik@vimn.com">Nicholls.Mark@vimn.com</a> T<b>:</b></span><span lang="EN-GB" style="font-size:8.0pt;color:#1F497D">
</span><span lang="EN-GB" style="font-size:8.0pt;font-family:"Tahoma","sans-serif";color:teal">+44 (0)203 580 2223<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB" style="font-size:10.0pt;color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB" style="color:#1F497D"><img border="0" width="386" height="84" id="Picture_x0020_2" src="cid:image001.png@01D08196.52715160" alt="Description: cid:image001.png@01CD488D.9204D030"></span><span style="color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="EN-GB"><o:p> </o:p></span></p>
</div>
<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>