> yeah, that is what I mean. however, since we don't have explicit type
> passing in haskell, reasoning about the lazyness of types would be quite
> tricky, leading to odd things like changing type signatures (without
> changing the underlying types) can change the behavior of a program.
You mean
On Tue, Oct 03, 2006 at 12:10:52PM +0200, [EMAIL PROTECTED] wrote:
> So you mean that
>
> id = /\a . \x :: a . x
>
> is /strict/ in its first argument, i.e. in the /type/ a. So to speak,
> type erasure is equivalent to strictness in all and every type argument.
> For an irrefutable existentia
John Meacham wrote:
> the reason being that id translates internally to
>
>> id = /\a . \x::a . x
>
> since you cannot pull out an appropriate type to pass to id without
> evaluating the 'irrefutable' pattern, you end up with _|_ instead of 4.
>
> basically, allowing irrefutable matching on e
> Thanks for asking!
> [...]
> Online algorithms do look like a good place to try to get some leverage
> from this, but we haven't really been in a position to experiment so
> far. I'm sure that will change.
Well, I asked because laziness with memoization gives a definite edge in
terms of algorit
On 9/30/06, [EMAIL PROTECTED] <[EMAIL PROTECTED]> wrote:
data Eq a b where Refl :: Eq a a
coerce :: Eq a b -> a -> b
coerce ~Refl x = x
But this works well with Leibniz-style equality (
http://homepage.mac.com/pasalic/p2/papers/thesis.pdf ), because the
Equality proof/term is actually us
Hi
[EMAIL PROTECTED] wrote:
To summarize, the main problem is to get a lazy/online algorithm (the
problem here falls into the "more haste, less speed" category) while
staying more type safe.
@Conor: how does this issue look like in Epigram?
Thanks for asking!
In the current Epigram prototy
> But that makes it refutable! For the above, either
>
> coerce _|_ x === x
>
> or the notation is being abused.
Making a pattern irrefutable does not mean that the function in question
will become lazy:
fromJust (~Just x) = x
fromJust _|_ === _|_
The point with coerce is that it looks v
Here is a formulation of what exactly I require from irrefutable pattern
matches for GADTs.
The problem arouse from the "Optimization problem" thread. In short,
here is a GADT-using, type safe version of Bertram's solution (without
balancing)
> -- a binary search tree with witness about its
>> {-# OPTIONS -fglasgow-exts #-}
>>
>> module Main where
>>
>> import Data.IORef
>>
>> data T a where
>> Li:: Int -> T Int
>> Lb:: Bool -> T Bool
>> La:: a -> T a
>>
>> writeInt:: T a -> IORef a -> IO ()
>> writeInt v ref = case v of
>> ~(Li x) -> writeIORef ref (1::Int)
>>
>
