Re: Why not allow empty record updates?
I wrote:
Yes. The translation of record updates given in the Report
makes perfect sense for {}. It is only forbidden by
n = 1, but no reason is given for that restriction.
d wagner wrote:
It doesn't make sense to me. The translation explodes a value into a case
statement over its constructors; what constructors do you use when you don't
know the type of the value?
When n = 1, you know the type of the value by looking where the field came
from, and hence which constructors to use in the case statement.
Well, yes, you need to know the type. That's why I asked
Simon if there is difficulty with implementation.
I do have an algorithm in mind, but it seemed silly for me
to write it out given that I know near zero about
the implementation details of GHC's type checker.
But if you insist, here is a rough sketch:
Replace each subexpression of the form e {} by
v' and add v = e to the let bindings, where v and v' are
fresh variables. Resolve the type. For any v that resolves
to an ADT (even if the types of its parameters are not
resolved), replace e {} in the original expression by
its case expansion. Repeat until all are resolved,
rejecting the program if an iteration does not resolve
any v. Resolve the final form of the expression one
more time to obtain its type.
Does this make any sense?
Thanks,
Yitz
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Why not allow empty record updates?
| Trouble is, what type does this have?
|f x = x {}
|
| Malcolm Wallace wrote:
| f :: a - a
|
| Ian Lynagh wrote:
| That wouldn't help the original poster, as it is incompatible with
| f :: Foo Clean - Foo Dirty
There are several different things going on in this thread.
1. What does f x = x {} mean? The report
http://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-490003.15
says we should treat it like
f x = case x of
C1 a b - C1 a b
C2 v - C2 v
but if there are no fields how do we know what C1 and C2 are? The whole
section only makes sense if you know x's type. So Malcolm's suggestion of f
:: forall a. a - a would be non-uniform with the non-empty cases.
When we *do* know the type then the above translation makes sense, and even
allows the
f :: Foo Clean - Foo Dirty
type-change. Now two further issues arise:
2. When do we know the type? If the type is supposed to come from an
enclosing type signature, to specify the type system one would need to specify
the way that type annotations propagate. This isn't impossible (we do it for
higher-rank types), but it seems like a big hammer for this particular nut.
3. Edward wants to maintain sharing, meaning presumably that no fresh record
is allocated. That makes sense, but sadly System FC (GHC's intermediate
language) has no way to express it. We'd need some new axioms claiming that
forall ab. Foo a ~ Foo b. But that's a question for another time. Moreover,
it affects non-record types just as much.
Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: encoding and paths, again
On 16/11/2011 08:09, Ganesh Sittampalam wrote: On 14/11/2011 14:47, Simon Marlow wrote: (1) Does Win32 need similar additions? I can't spot any substantial changes to it for Max's PEP383, but I'm not sure if any lower-level library changes might have affected it. No - Win32 file paths cannot by definition contain invalid Unicode. The existing Win32 library is fine. (2) What's the recommended way of doing the equivalent of getDirectoryContents for RawFilePath? Do we also need to add raw versins to the directory package? getDirectoryContents :: RawFilePath - IO [RawFilePath] [...] Thanks. One followup - in the Win32 case (where I guess we can still use the normal getDirectoryContents and get a FilePath), is it still necessary to re-encode the results to guarantee independence from the current settings (e.g. as proposed by Max in http://www.haskell.org/pipermail/glasgow-haskell-users/2011-November/021116.html), or do we just always get the original filename properly because of the way Windows handles paths? I think Max's answer above applies when you know that file paths on the disk are stored in a different encoding from the locale. This doesn't apply to Win32, where file paths are always UTF-16, with the encoding and decoding handled by the Win32 layer. In fact, if Max goes ahead and adds setFilesystemEncoding and setLocaleEncoding as he suggested, then this will get easier: you can just set the encoding to whatever you want before doing any file system operations. Sorry if all this is obvious but every time I think I understand Unicode I get proven wrong! I know the feeling :-( Cheers, Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Way to expose BLACKHOLES through an API?
On Tue, 2011-11-08 at 15:43 +, Simon Marlow wrote: Hmm, but there is something you could do. Suppose a thread could be in a mode in which instead of blocking on a BLACKHOLE it would just throw an asynchronous exception WouldBlock. Any computation in progress would be safely abandoned via the usual asynchronous exception mechanism, and you could catch the exception to implement your evaluateNonBlocking operation. I'm not sure this would actually be useful in practice, but it's certainly doable. The linux kernel folks have been discussing a similar idea on and off for the last few years. The idea is to return in another thread if the initial system call blocks. Perhaps there's an equivalent here. We have an evaluateThingy function and when the scheduler notices that thread is going to block for some reason (either any reason or some specific reason) we return from evaluateThingy with some info about the blocked thread. The thing that the kernel folks could never decide on was to do with thread identity: if it was the original thread that blocked and we return in a new thread, or if the original thread returns and a clone is the one that blocks. Or perhaps it's a crazy idea and it would never work at all :-) Duncan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Way to expose BLACKHOLES through an API?
Hi, On 16.11.2011, at 10:43, Duncan Coutts wrote: On Tue, 2011-11-08 at 15:43 +, Simon Marlow wrote: Hmm, but there is something you could do. Suppose a thread could be in a mode in which instead of blocking on a BLACKHOLE it would just throw an asynchronous exception WouldBlock. Any computation in progress would be safely abandoned via the usual asynchronous exception mechanism, and you could catch the exception to implement your evaluateNonBlocking operation. I'm not sure this would actually be useful in practice, but it's certainly doable. The linux kernel folks have been discussing a similar idea on and off for the last few years. The idea is to return in another thread if the initial system call blocks. Perhaps there's an equivalent here. We have an evaluateThingy function and when the scheduler notices that thread is going to block for some reason (either any reason or some specific reason) we return from evaluateThingy with some info about the blocked thread. The thing that the kernel folks could never decide on was to do with thread identity: if it was the original thread that blocked and we return in a new thread, or if the original thread returns and a clone is the one that blocks. The difference between the requirements of the Linux kernel folks and the OP is that in the Linux kernel the evaluation has to continue, while in the Haskell case we know that the BLACKHOLE is already evaluated by someone else. I am obviously no expert on the GHC internals, but that is what I understood by reading the papers about the runtime system. So, in GHC I'd say it would make sense to stay in the original thread and throw the exception as Simon Marlow said. Just my 2 eurocents. Cheers, Jean ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Way to expose BLACKHOLES through an API?
On 16/11/2011 10:20, Jean-Marie Gaillourdet wrote: Hi, On 16.11.2011, at 10:43, Duncan Coutts wrote: On Tue, 2011-11-08 at 15:43 +, Simon Marlow wrote: Hmm, but there is something you could do. Suppose a thread could be in a mode in which instead of blocking on a BLACKHOLE it would just throw an asynchronous exception WouldBlock. Any computation in progress would be safely abandoned via the usual asynchronous exception mechanism, and you could catch the exception to implement your evaluateNonBlocking operation. I'm not sure this would actually be useful in practice, but it's certainly doable. The linux kernel folks have been discussing a similar idea on and off for the last few years. The idea is to return in another thread if the initial system call blocks. Perhaps there's an equivalent here. We have an evaluateThingy function and when the scheduler notices that thread is going to block for some reason (either any reason or some specific reason) we return from evaluateThingy with some info about the blocked thread. The thing that the kernel folks could never decide on was to do with thread identity: if it was the original thread that blocked and we return in a new thread, or if the original thread returns and a clone is the one that blocks. The difference between the requirements of the Linux kernel folks and the OP is that in the Linux kernel the evaluation has to continue, while in the Haskell case we know that the BLACKHOLE is already evaluated by someone else. I am obviously no expert on the GHC internals, but that is what I understood by reading the papers about the runtime system. So, in GHC I'd say it would make sense to stay in the original thread and throw the exception as Simon Marlow said. We have a great solution to the thread identity problem already - just freeze the computation using an asynchronous exception, and return in the original thread. The freezing process stores the state of the computation (i.e. the stack) on the heap, where it can be resumed by just evaluating the same value again. So I'm still not sure why we would want to do this, and we need a concrete application to be sure that the design is useful. Ryan had some application in mind using lazy bytestrings, but I don't think I really understand how this scheme would help yet. Cheers, Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
heads up: GHC gets a new constraint solver (again)
Friends, After a very busy period of hard work with Simon, we've re-engineered GHCs constraint solver and I just pushed a big patch on master along with modifications in the testsuite. The new constraint solver is based on the existing in its core ideas but is shorter, much cuter, and for many programs much faster (for others performance is roughly the same) If you had a program that was taking very long to compile in the past, we'd be very interested to see how this reengineered constraint solver performs on it. Same if you spot problems or notable regressions. Thanks, enjoy! Dimitrios -Original Message- From: cvs-ghc-boun...@haskell.org [mailto:cvs-ghc-boun...@haskell.org] On Behalf Of dimit...@microsoft.com Sent: 16 November 2011 17:42 To: cvs-...@haskell.org Subject: [commit: ghc] master: GHC gets a new constraint solver. More efficient and smaller in size. (0007c0e) Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master http://hackage.haskell.org/trac/ghc/changeset/0007c0ec9c0de68e3a348b8c4 112ac48fd861b1e --- commit 0007c0ec9c0de68e3a348b8c4112ac48fd861b1e Author: Dimitrios Vytiniotis dimit...@microsoft.com Date: Wed Nov 16 16:12:48 2011 + GHC gets a new constraint solver. More efficient and smaller in size. compiler/basicTypes/DataCon.lhs |9 +- compiler/basicTypes/MkId.lhs | 10 +- compiler/codeGen/CgCase.lhs | 18 +- compiler/coreSyn/CoreLint.lhs| 78 +- compiler/coreSyn/CoreSubst.lhs | 15 +- compiler/coreSyn/CoreUtils.lhs | 27 +- compiler/deSugar/Desugar.lhs |7 +- compiler/deSugar/DsBinds.lhs | 29 +- compiler/deSugar/DsCCall.lhs |4 +- compiler/deSugar/DsUtils.lhs |2 +- compiler/hsSyn/HsBinds.lhs | 17 +- compiler/prelude/TysPrim.lhs | 12 +- compiler/simplCore/CoreMonad.lhs |9 +- compiler/simplCore/OccurAnal.lhs |4 +- compiler/simplCore/SimplUtils.lhs|2 +- compiler/simplCore/Simplify.lhs | 25 +- compiler/typecheck/Inst.lhs | 71 +- compiler/typecheck/TcCanonical.lhs | 1361 ++ compiler/typecheck/TcErrors.lhs | 48 +- compiler/typecheck/TcHsSyn.lhs | 12 +- compiler/typecheck/TcInteract.lhs| 1664 +- compiler/typecheck/TcMType.lhs | 40 +- compiler/typecheck/TcRnDriver.lhs| 15 +- compiler/typecheck/TcRnMonad.lhs |9 + compiler/typecheck/TcRnTypes.lhs | 194 +++- compiler/typecheck/TcSMonad.lhs | 1211 ++-- compiler/typecheck/TcSimplify.lhs| 522 + compiler/typecheck/TcSplice.lhs |2 +- compiler/typecheck/TcType.lhs| 41 +- compiler/types/Coercion.lhs | 99 +- compiler/types/FunDeps.lhs | 10 +- compiler/types/Type.lhs | 12 +- compiler/types/TypeRep.lhs | 21 +- compiler/vectorise/Vectorise/Type/PRepr.hs |4 +- compiler/vectorise/Vectorise/Utils/PADict.hs |2 +- 35 files changed, 3205 insertions(+), 2401 deletions(-) Diff suppressed because of size. To see it, use: git show 0007c0ec9c0de68e3a348b8c4112ac48fd861b1e ___ Cvs-ghc mailing list cvs-...@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: heads up: GHC gets a new constraint solver (again)
On Wednesday 16 November 2011, 19:22:53, Dimitrios Vytiniotis wrote: Friends, After a very busy period of hard work with Simon, we've re-engineered GHCs constraint solver and I just pushed a big patch on master along with modifications in the testsuite. The new constraint solver is based on the existing in its core ideas but is shorter, much cuter, and for many programs much faster (for others performance is roughly the same) If you had a program that was taking very long to compile in the past, we'd be very interested to see how this reengineered constraint solver performs on it. Same if you spot problems or notable regressions. Seems to be a clear win for T5030: bytes allocated 943772224 is less than minimum allowed 12 If this is because you have improved GHC, please update the test so that GHC doesn't regress again *** unexpected failure for T5030(normal) :D But due to its greater efficiency, it's dangerous in cases like SkolemOccursLoop. It seems the new solver gets as far with a context-stack of N as the old got with a context-stack of 2N+1 there. When, like in SkolemOccursLoop, the context grows exponentially in size, you're running out of memory even with a relatively small context-stack. Cheers, Daniel ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why not allow empty record updates?
On 11/15/11 8:07 PM, wagne...@seas.upenn.edu wrote:
Quoting wren ng thornton w...@freegeek.org:
So far I've just defined helper functions to adjust the phantom
type[1], each of which is implemented by (\x - x { foo = foo x }).
It's a horrible hack, but at least it's hidden away in library
functions instead of something I have to look at. The annoying part
(a bit tongue-in-cheek, and hence not sent to the mailing list)
Forwarding to the list, because I actually have a serious response :)
As long as we're writing hacks, why not use unsafeCoerce? ;-)
In this particular case I don't care too much about representation
sharing (though I do share Ed's concern), and I generally do my best to
avoid unsafeFoo just so I can minimize my personal proof obligations /
maximize the utility of the compiler's type checking.
Though, yes, in other projects with similar considerations I've also
gone the unsafeCoerce route. Other than invalidating type system
guarantees, it does have the side effect that it can interfere with
rewrite rules firing (since the coercion remains in the System Fc core).
And the times when I really care about representation sharing are often
also the times I really care about rewrite rules firing. Which in turn
means I tend to add additional rewrite rules to push the unsafeCoerce
around in order to get it out of the way so that other rules can fire.
But I see no way of specifying these additional rules in full generality
while retaining correctness--- without some additional mechanism to say
things like this newtype wrapper is opaque in these contexts (to
preserve the abstract semantics), but is translucent in these other
contexts (to abide by categorical laws like functorality). It's really
unfortunate that these complementary goals of sharing representation and
doing rewrites/fusion are at odds in current Haskell.
I run into similar issues with needing to work around coercions in Coq,
since they impede the evaluator and proofs of value equality due to the
weakness of Coq's case analysis. That the issue shows up in Coq as well
seems to imply that the root of the problem is something deeper than
noone having implemented the convenience. Agda has a stronger case
analysis and so doesn't run into quite the same issues, though I'm not
entirely clear on the exact ways in which Agda's case analysis gains
that extra power, so it's unclear whether we could (meaningfully) add
the power to Haskell without going whole hog into dependent types.
Of course, this all is related to the problem of strong updates; it just
happens that the update is Curry-identical, yet Church-different. Given
the general preference for Church-style lambda calculi, it's not
surprising that this exact problem hasn't been tackled (to my knowledge).
Another place this problem has come up for me is in wanting to ensure
representation sharing for values constructed by data constructors which
don't make use of their type parameters. A trivial example would be
sharing the representation of Nothing between all the Maybe types, or
sharing the empty list among all the list types. That example isn't
especially motivating, but there are other cases where we can end up
with a large structure for which the type parameters are 'phantom' even
though they may not be phantom in general (because other data
constructors make use of them). That we want type updates for records
with phantom types is just a symptom of the larger issue of wanting type
updates for all quasiphantom/pseudophantom types.
--
Live well,
~wren
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
