David Menendez wrote:
On Wed, Oct 1, 2008 at 7:53 PM, wren ng thornton <[EMAIL PROTECTED]> wrote:
[1] Just like existential types, you can put something in but you can never
get it back out again. For inescapable monads like IO and ST, this is why
they have the behavior of sucking your whole pro
On Wed, Oct 1, 2008 at 7:53 PM, wren ng thornton <[EMAIL PROTECTED]> wrote:
>
> [1] Just like existential types, you can put something in but you can never
> get it back out again. For inescapable monads like IO and ST, this is why
> they have the behavior of sucking your whole program into the exi
Jason Dagit wrote:
I was asserting that Haskell is currently 2 layered. Purely functional vs.
IO. They integrate nicely and play well together, but I still think of them
as distinct layers. Perhaps this is not fair or confusing though. The
paper I cited did indeed use codata to define streams
Jason Dagit wrote:
> apfelmus wrote:
>>
>> It seems to me that dependent types are best for ensuring totality.
>
> Bear with me, as I know virtual nothing about dependent types yet.
Ah, my bad. Time to change that ;) Personally, I found
Th. Altenkirch, C. McBride, J. McKinna.
Why dependent t
2008/9/30 Jason Dagit <[EMAIL PROTECTED]>:
>> It seems to me that dependent types are best for ensuring totality.
>
> Bear with me, as I know virtual nothing about dependent types yet. In the
> total functional paradigm the language lacks a value for bottom. This means
> general recursion is out
On Tue, Sep 30, 2008 at 12:51 AM, apfelmus <[EMAIL PROTECTED]>wrote:
> Jason Dagit wrote:
> > Hello,
> >
> > I recently had someone point me to this thread on LtU:
> > http://lambda-the-ultimate.org/node/2003
> >
> > The main paper in the article is this one:
> >
> http://www.jucs.org/jucs_10_7/to
Jason Dagit wrote:
> Hello,
>
> I recently had someone point me to this thread on LtU:
> http://lambda-the-ultimate.org/node/2003
>
> The main paper in the article is this one:
> http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf
>
> It leaves me with seve
