headers
Ashley Yakeley | 1 Feb 2007 01:51

Re: help from the community?

Taral wrote:

 > I see nothing wrong with "case x of {}", with required braces. The
 > layout rule never generates empty braces.

Also consider a simple "case x", following the already allowed omission 
of "where" in class and instance decls.

   class (This a,That a) => ThisThat a

   instance (This a,That a) => ThisThat a

This will be useful for GADTs:

   data MyGADT a where
     IntGADT :: MyGADT Int

   never :: MyGADT Char -> t
   never x = case x  -- no bottom needed

--

-- 
Ashley Yakeley
Permalink | Reply | 1 comment |
headers
Arie Peterson | 1 Feb 2007 02:54
Picon
Picon
Favicon

Alleged problems with equational reasoning caused by views

J. Garrett Morris wrote (to Bulat Ziganshin):

> Yes - you've reiterated Wadler's original design, with an automatic
> creation of a type class.  Erwig and Peyton-Jones, _Pattern Guards and
> Transformational Patterns_
> (http://research.microsoft.com/~simonpj/Papers/pat.htm) mentions
> problems with equational reasoning raised by this approach.

I just read this paper, in particular the part about the problems with
equational reasoning that come up once you introduce (a certain form of)
views.

I fail to appreciate those problems. Perhaps someone can help me see them?
:-)

### Polar representation

Before taking on the problematic 'Half', I review the earlier example of
the polar representation of complex numbers.

> data Complex = Cart Float Float
>
> view Polar of Complex = Polar Float Float where
>   polar (Cart r i) = Polar (sqrt(r*r+i*i)) (atan2 r i)

I am slightly puzzled by this notation: the role of the extra function (?)
'polar' is unclear to me. If I leave it out, the definition makes sense:

  'Cart r i' and 'Polar (sqrt(r*r+i*i)) (atan2 r i)' are declared to be
the same object.
(Continue reading)

Permalink | Reply | 1 comment |
headers
Conor McBride | 1 Feb 2007 07:08
Picon

Re: help from the community?

Hi

Ashley Yakeley wrote:
> Taral wrote:
>
> > I see nothing wrong with "case x of {}", with required braces. The
> > layout rule never generates empty braces.
>
> Also consider a simple "case x",

[..]

> This will be useful for GADTs:
>
>   data MyGADT a where
>     IntGADT :: MyGADT Int
>
>   never :: MyGADT Char -> t
>   never x = case x  -- no bottom needed

I like it, but I might like it even more if there was a little more noise
  (1) to distinguish this syntax from a lapse of concentration
  (2) to indicate that the construct is (morally) strict, well-defined 
because x is undefined;
       remember, case undefined { _ -> () } is ().

I don't like "case x of {}", because it's just another way of saying 
"undefined", ie "x might have cases but we're not going to handle any of 
them". If there was some total variant, "cover" of case whose coverage 
was enforced, I'd be happy with "cover x of {}".
(Continue reading)

Permalink | Reply | 0 comments |
headers
Bulat Ziganshin | 1 Feb 2007 10:56
Picon

Re[4]: ADT views Re: [Haskell] Views in Haskell

Hello J.,

Thursday, February 1, 2007, 1:36:33 AM, you wrote:

> Yes - you've reiterated Wadler's original design, with an automatic

> problems with equational reasoning raised by this approach.

ok, i can live without it. i mean reasoning :)

i guess that anything more complex than Turing machine makes reasoning
harder. 18 years ago Haskell fathers chosen to simpilfy language in
order to make reasoning easier. may be now we can change this
decision? that i've proposed is made on basis of my 15 years of
software development experience and i'm sure that abstraction of data
representation is very important issue (and much more important than
reasoning for practical programming)

--

-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin@...
Permalink | Reply | 3 comments |
headers
Yitzchak Gale | 1 Feb 2007 11:13

Global variables

The trick of controlling allocation of external
resources by using NOINLINE, unsafePerfromIO,
and IORef to create global variables has become
an indispensable technique in Haskell. It seems to
work well enough with most current compilers.

However, it is well known that the semantics of
NOINLINE are not sufficient to guarantee that this
is safe. In principle, the runtime is permitted to
GC and reinstantiate these things at any time.

Also, it would be nice if we could have a
guarantee that global constants are not instantiated
until first use. That would allow us to skip the
IORef in some cases.

I think this issue needs to be addressed in Haskell'.
(If it has already, please accept my apologies.)
Since NOINLINE has more general use, perhaps
there should be a new pragma for this purpose.

Thanks,
Yitz
Permalink | Reply | 7 comments |
headers
Arie Peterson | 1 Feb 2007 12:08
Picon
Picon
Favicon

Re: ADT views

Bulat Ziganshin wrote:

> ok, i can live without it. i mean reasoning :)
>
> i guess that anything more complex than Turing machine makes reasoning
> harder. 18 years ago Haskell fathers chosen to simpilfy language in
> order to make reasoning easier. may be now we can change this
> decision? that i've proposed is made on basis of my 15 years of
> software development experience and i'm sure that abstraction of data
> representation is very important issue (and much more important than
> reasoning for practical programming)

No. Abstractions should (and mostly do) make reasoning easier, not harder,
by having clear semantics, suited to the problem domain.

The ability to reason about your program is vital in about every part of
the programming cycle, and is one of the things that make Haskell work.

Another of those things is abstraction of data representation, you're
right about that. But I think there is no conflict between those goals.

In fact, all the views proposal does is to give the natural meaning to the
equation

> f (v x) = h x

, by letting the programmer specify a partial inverse for 'v'.

Greetings,
(Continue reading)

Permalink | Reply | 1 comment |
headers
Jón Fairbairn | 1 Feb 2007 12:26
X-Face
Picon
Picon
Favicon

A view of views -- something classy? Re: [Haskell] Views in Haskell


Bulat Ziganshin
<bulat.ziganshin@...>
writes:
> > Yes - you've reiterated Wadler's original design, with
> > an automatic problems with equational reasoning raised
> > by this approach.
> 
> ok, i can live without it. i mean reasoning :)

That's probably not good, but I don't follow that problem
yet.  I'm afraid I've not had the stamina to follow this
thread properly, and I doubt if I'll get any more stamina
soon, so let me make a proposal not too disimilar to Bulat's
and just hope that people find it appealing enough to flesh
it out.

The idea I'm presenting is simple enough: allow data
constructors as members of classes.  (Sure, David, this does
have the problem of hiding potentially expensive operations
as straightforward pattern matches, but that's abstraction
for you). So

class Sequence s where
   (some other stuff)
   Cons:: a -> s a -> s a
   Nil:: s a

Here Cons and Nil both stand for two things: a constructor
and a deconstructor. The question is how to specify the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Brian Hulley | 1 Feb 2007 12:40

Re: help from the community?

Taral wrote:
> On 1/31/07, Conor McBride <ctm@...> wrote:
>> So, as far as Haskell' is concerned, I'd favour forbidding non-empty
>> cases, but only because I favour having some more explicit syntax for
>> empty cases, further down the line.
>
> I see nothing wrong with "case x of {}", with required braces. The
> layout rule never generates empty braces.

main = do
                a <- do
                            b <- something
                            case b of
                return a

Doesn't the layout rule convert the above to:

main = do { a <- do { b <- something; case b of {}}; return a}
                                                                          ^^ 
empty braces

In any case I thought the layout rule was supposed to be regarded as just a 
convenience rather than making a distinction between explicit braces and 
braces added by the rule?

Also, can anyone explain why empty case constructs are needed? Why not just 
write undefined?

Brian.
--

--
(Continue reading)

Permalink | Reply | 0 comments |
headers
Bulat Ziganshin | 1 Feb 2007 11:27
Picon

Re: Global variables

Hello Yitzchak,

Thursday, February 1, 2007, 1:13:48 PM, you wrote:

there is common proposal that i support. example of its use:

i :: IORef Int
i <- newIORef 1

with a semantics equivalent to current use of usafePerformIO+INLINE in GHC

--

-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin@...
Permalink | Reply | 6 comments |
headers
Bulat Ziganshin | 1 Feb 2007 12:47
Picon

Re[2]: ADT views

Hello Arie,

Thursday, February 1, 2007, 2:08:33 PM, you wrote:

> The ability to reason about your program is vital in about every part of
> the programming cycle, and is one of the things that make Haskell work.

when i say what i don't use reasoning, you can trust me :)

> Another of those things is abstraction of data representation, you're
> right about that. But I think there is no conflict between those goals.

right now we are discussing such conflict, not be? :)

--

-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin@...
Permalink | Reply | 0 comments |

Gmane