On Thu, Sep 28, 2006 at 03:22:25PM +0100, Simon Peyton-Jones wrote:
> | Does anything go wrong with irrefutable patterns for existential
> types?
>
> Try giving the translation into System F.
Hmm, that's not quite as satisfying as Conor's answer for GADTs.
___
| Does anything go wrong with irrefutable patterns for existential
types?
Try giving the translation into System F.
Simon
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
On Tue, Sep 19, 2006 at 01:52:02PM +0100, Conor McBride wrote:
> [EMAIL PROTECTED] wrote:
> >Btw, why are there no irrefutable patterns for GADTs?
>
> Just imagine
>
> > data Eq a b where Refl :: Eq a a
>
> > coerce :: Eq a b -> a -> b
> > coerce ~Refl a = a
>
> coerce undefined True :: String
On Tue, Sep 19, 2006 at 08:06:07PM +0200, [EMAIL PROTECTED] wrote:
> For our optimization problem, it's only a matter of constructors on the
> right hand side. They should pop out before do not look on any
> arguments, so it's safe to cry "so you just know, i'm a Just".
It seems the appropriate en
Robert Dockins wrote:
On Sep 19, 2006, at 8:52 AM, Conor McBride wrote:
Hi folks
[EMAIL PROTECTED] wrote:
Btw, why are there no irrefutable patterns for GADTs? I mean, such a
sin
should be shame for a non-strict language...
Just imagine
> data Eq a b where Refl :: Eq a a
> coerce :: E
On Sep 19, 2006, at 8:52 AM, Conor McBride wrote:
Hi folks
[EMAIL PROTECTED] wrote:
Btw, why are there no irrefutable patterns for GADTs? I mean, such
a sin
should be shame for a non-strict language...
Just imagine
> data Eq a b where Refl :: Eq a a
> coerce :: Eq a b -> a -> b
> coer
Hi folks
[EMAIL PROTECTED] wrote:
Btw, why are there no irrefutable patterns for GADTs? I mean, such a sin
should be shame for a non-strict language...
Just imagine
> data Eq a b where Refl :: Eq a a
> coerce :: Eq a b -> a -> b
> coerce ~Refl a = b
coerce undefined True :: String
Bang
On Tue, Sep 19, 2006 at 01:41:51PM +0200, [EMAIL PROTECTED] wrote:
> Btw, why are there no irrefutable patterns for GADTs?
Not GADTs, but existential types (whether done with GADTs or not).
They can't be analysed with irrefutable patterns, of which let bindings
are a special case:
http://www.hask
On Mon, Sep 18, 2006 at 12:23:11AM +0100, Ross Paterson wrote:
> To prove that (even for partial and infinite lists ps)
>
> splitSeq ps = [(a, seconds a ps) | a <- nub ps]
>
> [...] we can establish, by induction on the input list,
>
> (1) fst (splitSeq' s ps) =
> [(a, seco
On Sun, Sep 17, 2006 at 01:08:04PM +0200, [EMAIL PROTECTED] wrote:
> Ross Paterson wrote:
> > It's interesting that these composed transformations don't seem to cost
> > too much.
>
> That the composed transformations are indeed cheap is not necessarily
> disturbing.
I meant the composition of th
ross:
> On Thu, Sep 14, 2006 at 07:51:59PM +0200, Bertram Felgenhauer wrote:
> > It's a result of thinking about lazy evaluation, and
> > especially lazy patterns (and let bindings) for some time. A wiki article
> > that helped me a lot to understand these is
> >
> > http://www.haskell.org/hawik
On Thu, Sep 14, 2006 at 07:51:59PM +0200, Bertram Felgenhauer wrote:
> It's a result of thinking about lazy evaluation, and
> especially lazy patterns (and let bindings) for some time. A wiki article
> that helped me a lot to understand these is
>
> http://www.haskell.org/hawiki/TyingTheKnot
>
On Thu, 14 Sep 2006, Bertram Felgenhauer wrote:
> Magnus Jonsson wrote:
> > Thanks Bertran for your solution. I have difficulty understanding it so I
> > can't comment on it right now but I'll try to have a look at it. Do you
> > know of any article that explains this technique, starting from v
Magnus Jonsson wrote:
> Thanks Bertran for your solution. I have difficulty understanding it so I
> can't comment on it right now but I'll try to have a look at it. Do you
> know of any article that explains this technique, starting from very
> simple examples?
Not really. It's a result of thin
Thanks Bertran for your solution. I have difficulty understanding it so I
can't comment on it right now but I'll try to have a look at it. Do you
know of any article that explains this technique, starting from very
simple examples?
/Magnus
On Thu, 14 Sep 2006, Bertram Felgenhauer wrote:
I w
15 matches
Mail list logo