#6018: Injective type families
-------------------------------+-------------------------------------------
Reporter: lunaris | Owner: simonpj
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies, Injective
Resolution: | Architecture: Unknown/Multiple
Operating System: | Difficulty: Unknown
Unknown/Multiple | Blocked By:
Type of failure: | Related Tickets: #4259
None/Unknown |
Test Case: |
Blocking: |
-------------------------------+-------------------------------------------
Comment (by hpacheco):
To get going, I wouldn't mind if the onus of proving that the type family
is indeed injective fell on me, in an unsafe way.
But I understand that it is clearly not a feature that you should blindly
introduce in mainstream GHC...
I may look into it in the future if I ever find the time, but I doubt it.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:30>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------+-------------------------------------------
Reporter: lunaris | Owner: simonpj
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies, Injective
Resolution: | Architecture: Unknown/Multiple
Operating System: | Difficulty: Unknown
Unknown/Multiple | Blocked By:
Type of failure: | Related Tickets: #4259
None/Unknown |
Test Case: |
Blocking: |
-------------------------------+-------------------------------------------
Comment (by simonpj):
I don't think anyone is working on injective type families right now, but
it would make a good project, and not too difficult.
Lunaris's patch has a lot of irrelevant white-space changes in it. But
the biggest problem is that I don't think it implements the all-important
check that a injective type family really is injective. Consider
{{{
injective type family F a
type instance F Int = Bool
type instance F Char = Bool
}}}
This isn't injective and should jolly well be rejected. And this should
be the case even if the two `type instance` declarations are in different
modules.
Similar code already exist for rejecting type-family ''overlap''; I think
it is in `FamInst.checkFamInstConsistency`. But it'd need to be beefed up
to deal with the injectiveness check.
And you need to take care. What about
{{{
type instance F Int = Bool -- (BAD)
type instance F Char = F Int -- (BAD)
}}}
The two RHSs look different, but actually they are the same. The
criterion for injectivity is that
{{{
If (F t1 .. tn) ~ (F s1 .. sn)
then t1 ~ s1
...
tn ~ sn
}}}
That doesn't hold for the (BAD) instances, so they should be rejected. In
the terminology of the "Closed type families" paper, we need the two RHSs
to be '''apart'''.
Simon
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:29>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#4934: threadWaitRead works incorrectly on nonthreaded RTS
------------------------------------------------+--------------------------
Reporter: slyfox | Owner:
Type: bug | Status: patch
Priority: normal | Milestone: ⊥
Component: Runtime System | Version: 7.0.1
Resolution: | Keywords:
Operating System: Linux | Architecture: x86_64
Type of failure: Incorrect result at runtime | (amd64)
Test Case: | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
------------------------------------------------+--------------------------
Comment (by slyfox):
> Yes, please squash the patches and then I'll review.
Will do.
> Not sure what you mean by "slightly change polling cycle to resume only
descriptors with data available", don't we already do that?
I was a bit unclear. I meant: only in a case of '''select() == EBADF'''
failure we
always resumed all the blocked threads:
https://ghc.haskell.org/trac/ghc/browser/ghc/rts/posix/Select.c#L295
{{{
if ( errno == EBADF )
unblock_all = rtsTrue;
...
ready = unblock_all || FD_ISSET(tso->block_info.fd, &rfd); // [1]
...
if (ready)
pushOnRunQueue(&MainCapability,tso);
}}}
Current patchset only propagates exceptions early,
but does not fix spurious resumes (as it was before).
I propose to fix resume problem:
{{{
--- ready = unblock_all || FD_ISSET(tso->block_info.fd, &rfd);
+++ if (unblock_all) ready = fd_is_really_ready (fd);
+++ else ready = FD_ISSET(tso->block_info.fd, &rfd);
}}}
It' won't be hard to implement on top of current patchset.
Secondary '''select()''' can already provide all the info.
Should I do it as a) a separate patch/ticket, b) merge into final result,
c) don't touch it at all?
Thanks!
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/4934#comment:23>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#4934: threadWaitRead works incorrectly on nonthreaded RTS
------------------------------------------------+--------------------------
Reporter: slyfox | Owner:
Type: bug | Status: patch
Priority: normal | Milestone: ⊥
Component: Runtime System | Version: 7.0.1
Resolution: | Keywords:
Operating System: Linux | Architecture: x86_64
Type of failure: Incorrect result at runtime | (amd64)
Test Case: | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
------------------------------------------------+--------------------------
Comment (by simonmar):
Yes, please squash the patches and then I'll review.
Not sure what you mean by "slightly change polling cycle to resume only
descriptors with data available", don't we already do that?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/4934#comment:22>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#4934: threadWaitRead works incorrectly on nonthreaded RTS
------------------------------------------------+--------------------------
Reporter: slyfox | Owner:
Type: bug | Status: patch
Priority: normal | Milestone: ⊥
Component: Runtime System | Version: 7.0.1
Resolution: | Keywords:
Operating System: Linux | Architecture: x86_64
Type of failure: Incorrect result at runtime | (amd64)
Test Case: | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
------------------------------------------------+--------------------------
Comment (by slyfox):
If idea in patches looks fine i can squash last 3 patches in one and
cleanup comments around.
I can also slightly change polling cycle to resume only descriptors with
data available,
and not all the waiters. It would be more robust against spurious blocking
calls.
What do you think?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/4934#comment:21>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#4934: threadWaitRead works incorrectly on nonthreaded RTS
------------------------------------------------+--------------------------
Reporter: slyfox | Owner:
Type: bug | Status: new
Priority: normal | Milestone: ⊥
Component: Runtime System | Version: 7.0.1
Resolution: | Keywords:
Operating System: Linux | Architecture: x86_64
Type of failure: Incorrect result at runtime | (amd64)
Test Case: | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
------------------------------------------------+--------------------------
Comment (by slyfox):
After throwToSingleThreaded '''tso''' should not be pushed to runnables
queue.
0004-rts-posix-Select.c-don-t-put-thread-with-pending-exc.patch fixes this
problem.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/4934#comment:19>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
