> So, either the interpretation of the isomorphism is wrong, or Haskell
> type syste m is in fact unsound. Right ?
> They cannot be both true!
Let us indeed examine what exactly it means for a type system to be
sound. The soundness of a type system is usually proved as a theorem
of a form:
Hi there.
I got this question while I'm messing around with my toy monad.
I was thinking about creating a generic monad that can persist state change
even when fail is called. The StateT monad will discard the state change so
it makes it hard to add tracing to the program. (at least to me. If
Double is a pretty poor choice of "whatever" (just thinking about
equality of floating point numbers puts one in a state of sin :-)).
Worse still, your newChanSafe would be type-unsafe if you gave it that
polymorphic type (think about it).
So let's assume channels aren't polymorphic and that we
[Early registration deadline: 14 May 2004.]
Call for Participation
AFP 2004
5th International Summer School on
Advanced Functional Programming
Tartu, Estonia
Greetings [and apologies if you get multiple copies]:
The fifth ACL2 Workshop will be held November 18-19, 2004, in Austin Texas,
USA, in conjunction with (and immediately following) FMCAD. We invite users
of ACL2, users of other theorem provers, and persons interested in the
applications of theo
Yes, that makes sense, but I'm ok with passing in
an identity. I'd like a function like this:
newChanSafe::Identity -> Chan a
type Identity = Double -- or whatever
-Alex-
_
S. Alexander Jacobson mailto:[EMAIL
Channels have identity, so allocating a new one is a side effecting
operation. Having it outside the IO monad would require (for example):
(newChan, newChan) = (let x = newChan in (x,x))
which is wrong. If you wrap newChan in unsafePerformIO then the compiler
will feel free to apply rewrites like
S. Alexander Jacobson wrote:
Nothing actually happens when newChan is called
except construction of a new datastructure. It
would be nice to have non IO monad code be able to
create a new Chan that gets passed to IO code that
uses it somewhere else.
Alternatively, is there a way to create a Cha
Nothing actually happens when newChan is called
except construction of a new datastructure. It
would be nice to have non IO monad code be able to
create a new Chan that gets passed to IO code that
uses it somewhere else.
Alternatively, is there a way to create a Chan
outside the IO monad?
-Alex-
On Fri, 23 Apr 2004, Bruno Oliveira wrote:
> and haskell type system is sound
>
> then we cannot write coerce.
>
> Which as been shown in the last emails that it is not true.
>
> So, either the interpretation of the isomorphism is wrong, or Haskell
> type system is in fact unsound. Right ? They ca
Hi Frank!
But then I have a paradox ...
coerce :: a -> b
coerce x = undefined
As an obvious consequence, Haskell type system would be unsound.
So, I assumed that this would be a wrong interpretation.
>>
>>> This is the part of your email which frightens me the most.
coerce :: a -> b
coerce x = undefined
As an obvious consequence, Haskell type system would be unsound.
So, I assumed that this would be a wrong interpretation.
This is the part of your email which frightens me the most. Of
course Haskell's type system is unsound! What factors lead you to
this kin
On 23/04/2004, at 10:56 PM, Bruno Oliveira wrote:
but then, it would be too easy to write this in haskell:
coerce :: a -> b
coerce x = undefined
As an obvious consequence, Haskell type system would be unsound.
So, I assumed that this would be a wrong interpretation.
This is the part of your emai
Tomasz Zielonka wrote:
On Fri, Apr 23, 2004 at 03:32:54AM +0200, Sebastian Sylvan wrote:
First you need to parse the expression into a Haskell data type. For
this I would recommend Parsec (see Haskell.org). The Haskell data type
would be something like
data Expr = AtomD Double | AtomI Intege
Hi!
Thanks Connor, I enjoyed your answer, it was very illustrative.
>> but then, it would be too easy to write this in haskell:
>>
>> coerce :: a -> b
>> coerce x = undefined
>>
>> As an obvious consequence, Haskell type system would be unsound.
>>
>> So, I assumed that this would be a wrong i
JP Bernardy wrote:
I'd say, check what any primitive 'proves' before
using it. Besides that, calling other functions is ok.
Except for general recursion.
coerce :: a -> b
coerce = coerce
-- Lennart
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.h
Hi,
--- Bruno Oliveira <[EMAIL PROTECTED]>
wrote:
> coerce :: a -> b
> coerce x = undefined
>
> As an obvious consequence, Haskell type system would
> be unsound.
Actually, in the isomrphism, "undefined" is a proof
that any theorem is correct. Somehow it can represent
an assumption that a subth
On Fri, Apr 23, 2004 at 03:32:54AM +0200, Sebastian Sylvan wrote:
>
> First you need to parse the expression into a Haskell data type. For
> this I would recommend Parsec (see Haskell.org). The Haskell data type
> would be something like
>
> data Expr = AtomD Double | AtomI Integer | Add Expr E
18 matches
Mail list logo
