<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Just thinking out loud, but if there were a way to generate
top-level definitions and datatypes from TC and if IO were possible
in TC, one could implement Type Providers [1] that way. E.g.
generate types+functions from a REST API definition at compile time.
If its a good idea is another question....<br>
<br>
Philipp<br>
<br>
[1]
<a class="moz-txt-link-freetext" href="https://docs.microsoft.com/en-us/dotnet/articles/fsharp/tutorials/type-providers/">https://docs.microsoft.com/en-us/dotnet/articles/fsharp/tutorials/type-providers/</a><br>
<br>
<div class="moz-cite-prefix">On 10/14/2016 01:22 PM, Ulf Norell
wrote:<br>
</div>
<blockquote
cite="mid:CAJjNqYEQBFfcb9pPPvdU_J-=Md8NNnrw81gJ2HdWVO_jwxucpA@mail.gmail.com"
type="cite">
<div dir="ltr">What's your use case? Agda IO is implemented using
the FFI so calling arbitrary IO functions from TC is not
possible. Internally TC runs on top of IO though, so if you have
a particular IO function in mind it could conceivably be added
as a primitive.
<div><br>
</div>
<div>/ Ulf</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Fri, Oct 14, 2016 at 9:54 AM, Roman
<span dir="ltr"><<a moz-do-not-send="true"
href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">Sorry for
the off-topic, but is it possible to run a TC computation<br>
inside the IO monad? Would be nice to type check terms that
come from<br>
IO in IO.<br>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>