January 2001 - Haskell-Cafe

Re: Type Pattern-Matching for Existential Types
by Ashley Yakeley 31 Jan '01

31 Jan '01

At 2001-01-30 22:16, Lennart Augustsson wrote: >It has large and horrible implications. To do dynamic type tests you need >to carry around the types at runtime. This is not something that Haskell >does (at least you don't have to). Hmm. In this: -- data Any = forall a. Any a a1 = Any 3 a2 = Any 'p' -- ...are you saying that a1 and a2 do not have to carry types at runtime? -- Ashley Yakeley, Seattle WA

3 2

Re: Type Pattern-Matching for Existential Types
by C.Reinke 31 Jan '01

31 Jan '01

> > > data Any = forall a. Any a > > > > > > get :: Any -> Maybe Char > > > get (Any (c::Char)) = Just c -- bad > > > get _ = Nothing .. > It can also be questioned from a software engineering standpoint. Much > of the purpose with existential types is to provide information hiding; > that is, the user of an existentially quantified type is not supposed to > know its concrete representation. The merits of an information hiding > dicipline is probably no news to anybody on this list. This discussion reminds me of an old paper by MacQueen: David MacQueen. Using dependent types to express modular structure. In Proc. 13th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 277--286, January 1986. He discusses some of the disadvantages of using plain existential quantification for modular programming purposes and proposes an alternative based on dependent sums, represented as pairing the witness type with the expression in which it is used, instead of existentials, where there is no witness for the existentially quantified type. See CiteSeer for some of the follow-on work that references MacQueen's paper: http://citeseer.nj.nec.com/context/32982/0 Some of that work tried to find a balance between having no witness types and carrying witness types around at runtime. In this context, Claudio Russo's work might be of interest, as he proposes to avoid the problems of existentials without going into (value-)dependent types: http://www.dcs.ed.ac.uk/home/cvr/ Claus

1 0

Type Pattern-Matching for Existential Types
by Ashley Yakeley 31 Jan '01

31 Jan '01

At 2001-01-30 19:52, Fergus Henderson wrote: >On 30-Jan-2001, Ashley Yakeley <ashley(a)semantic.org> wrote: >> At 2001-01-30 02:37, Fergus Henderson wrote: >> >> >class BaseClass s where >> > downcast_to_derived :: s -> Maybe Derived >> >> Exactly what I was trying to avoid, since now every base class needs to >> know about every derived class. This isn't really a practical way to >> build an extensible type hierarchy. > >Right. > >I don't know of any way to do that in Hugs/ghc without the problem that >you mention. Really it needs language support, I think. >(I have no idea if you can do it in O'Haskell.) It can't be done in O'Haskell either... Given that we have existential types, it would be nice to have a pattern-matching mechanism to get at the inside value. Something like... -- data Any = forall a. Any a get :: Any -> Maybe Char get (Any (c::Char)) = Just c -- bad get _ = Nothing -- ...but as it stands, this is not legal Haskell, according to Hugs: ERROR "test.hs" (line 4): Type error in application *** Expression : Any c *** Term : c *** Type : Char *** Does not match : _0 *** Because : cannot instantiate Skolem constant This, of course, is because the '::' syntax is for static typing. It can't be used as a dynamic pattern-test. Question: how big of a change would it be to add this kind of pattern matching? Is this a small issue, or does it have large and horrible implications? -- Ashley Yakeley, Seattle WA

4 4

Re: Type Pattern-Matching for Existential Types
by Ashley Yakeley 31 Jan '01

31 Jan '01

At 2001-01-30 23:11, Johan Nordlander wrote: >However, this whole idea gets forfeited if it's possible to look behind >the abstraction barrier by pattern-matching on the representation. Isn't this information-hiding more appropriately achieved by hiding the constructor? -- data IntOrChar = MkInt Int | MkChar Char data Any = forall a. MkAny a -- Surely simply hiding MkInt, MkChar and MkAny prevents peeking? -- Ashley Yakeley, Seattle WA

2 1

Re: O'Haskell OOP Polymorphic Functions
by Ashley Yakeley 30 Jan '01

30 Jan '01

At 2001-01-30 02:37, Fergus Henderson wrote: >class BaseClass s where > downcast_to_derived :: s -> Maybe Derived Exactly what I was trying to avoid, since now every base class needs to know about every derived class. This isn't really a practical way to build an extensible type hierarchy. -- Ashley Yakeley, Seattle WA

2 1

Re: O'Haskell OOP Polymorphic Functions
by Ashley Yakeley 30 Jan '01

30 Jan '01

At 2001-01-17 17:03, Lennart Augustsson wrote: >You seem to want dynamic type tests. This is another feature, and >sometimes a useful one. But it requires carrying around types at >runtime. Yes. I tried to do that myself by adding a field, but it seems it can't be done. >You might want to look at existential types; it is a similar feature. I seem to run into a similar problem: -- class BaseClass s data Base = forall a. BaseClass a => Base a class (BaseClass s) => DerivedClass s data Derived = forall a. DerivedClass a => Derived a upcast :: Derived -> Base upcast (Derived d) = Base d downcast :: Base -> Maybe Derived -- How do I define downcast? -- Ashley Yakeley, Seattle WA

3 3

HScript
by Eric Allen Wohlstadter 30 Jan '01

30 Jan '01

I have tried e-mailing the authors of HScript with my problems but they seem unresponsive. I was hoping maybe someone out there could help me. When I tried to run the demos I got an error "Could not find Prelude.hs", so I changed the hugsPath variable in regedit to point to hugs/lib. Then I got an error "Could not find Int". So I added hugs/lib/exts. Now I get the error "Addr.hs (line 23): Unknown primitive reference to addrToInt". Eric Wohlstadter

2 1

Re: 'any' and 'all' compared with the rest of the Report
by Jan-Willem Maessen 28 Jan '01

28 Jan '01

Bjorn Lisper <lisper(a)it.kth.se> replies to my reply: > >My current work includes [among other things] ways to eliminate this > >problem---that is, we may do a computation eagerly and defer or > >discard any errors. > > What you basically have to do is to treat purely data-dependent errors (like > division by zero, or indexing an array out of bounds) as values rather than > events. Indeed. We can have a class of deferred exception values similar to IEEE NaNs. [later]: > Beware that some decisions have to be taken regarding how error > values should interact with bottom. (For instance, should we have > error + bottom = error or error + bottom = bottom?) The choice affects which > evaluation strategies will be possible. Actually, as far as I can tell we have absolute freedom in this respect. What happens when you run the following little program? \begin{code} forever x = forever x bottomInt :: Int bottomInt = error "Evaluating bottom is naughty" + forever () main = print bottomInt \end{code} I don't know of anything in the Haskell language spec that forces us to choose whether to signal the error or diverge in this case (though it's clear we must do one or the other). Putting strong constraints on evaluation order would cripple a lot of the worker/wrapper-style optimizations that (eg) GHC users depend on for fast code. We want the freedom to demand strict arguments as early as possible; the consequence is we treat all bottoms equally, even if they exhibit different behavior in practice. This simplification is a price of "clean equational semantics", and one I'm more than willing to pay. -Jan-Willem Maessen jmaessen(a)mit.edu [PS - I've deliberately dodged the issue of program-level exception handling mechanisms and the like.]

3 3

Re: A clarification...
by Jan-Willem Maessen 26 Jan '01

26 Jan '01

qrczak(a)knm.org.pl (Marcin 'Qrczak' Kowalczyk) further clarifies my clarification: > > case ERROR of x -> expr => ERROR glb expr[?/x] > > The subject of errors vs. bottoms is discussed in > http://research.microsoft.com/~simonpj/papers/imprecise-exceptions.ps.gz Indeed. I crawled through my stack of electronic papers, and couldn't find the reference. As I noted in my earlier messages, I was deliberately dodging the issue of *catching* exceptions, as it really requires a thorough treatment. :-) The "?" in the above reduction is their special 0 term. They equate divergence with exceptional convergence within the functional calculus for the reasons I outlined [I reconstructed those reasons from memory and my own experience, so differences are due to my faulty recollection]. Their notion of refinement justifies the reduction I mentioned in my mail: > > case ERROR of x -> expr => ERROR In all, an excellent paper for those who are interested in this topic. -Jan-Willem Maessen

1 0

A clarification...
by Jan-Willem Maessen 26 Jan '01

26 Jan '01

Marko Schuetz <MarkoSchuetz(a)web.de> replies to me as follows: > > He uses this, and an argument based on currying, to show that strict > > functions ought to force their arguments left to right. > > I can't see where I did. I argued that distinguishing between error > and bottom seems to not leave much choice for bottom + error. You're right, sorry. I misread the following from your earlier message: > So I'd say error + bottom \equiv bottom and bottom + error \equiv > bottom. As you noted: > and you want, say, error + bottom \equiv error then + can no longer be > strict in its second argument.... I'd managed to turn this around in my head. Nonetheless, my fundamental argument stands: If we separate "bottom" and "error", we have a few choices operationally, and I'm not fond of them: 1) Make "error" a representable value. This appears closest to what you were describing above: case ERROR of x -> expr => expr [ERROR/x] This is tricky for unboxed types (especially Ints; floats and pointers aren't so hard; note that we need more than one distinguishable error value in practice if we want to tell the user something useful about what went wrong). At this point, by the way, it's not a big leap to flatten the domain as is done with IEEE NaNs, so that monotonicity wrt errors is a language-level phenomenon rather than a semantic one and we can handle exceptions by testing for error values. 2) Weaken the algebraic theory as I discussed in my last message. 3) Reject an operational reading of "case" as forcing evaluation and continuing and have it "do something special" when it encounters error: case ERROR of x -> expr => ERROR glb expr[?/x] >From the programmer's perspective, I'd argue that it's *better* to signal signal-able errors whenever possible, rather than deferring them. If nothing else, a signaled error is easier to diagnose than nontermination! Thus, I'd LIKE: error + bottom === error But I'm willing to acknowledge that I can't get this behavior consistently, except with some sort of fair parallel execution. I'm doing something along the lines of (3), but I abandon execution immediately on seeing error---which is consistent only if error==bottom: case ERROR of x -> expr => ERROR [Indeed, the compiler performs this reduction statically where possible, as it gets rid of a lot of dead code.] I defer the signaling of errors only if the expression in question is being evaluated eagerly; for this there is no "case" construct involved. -Jan-Willem Maessen

2 1