Left-to-right bias in type checking GADT functions
Hi all,
I have to admit that I haven't checked if this is a known issue...
The following is tested with both GHC 6.4.1 and 6.4.2; I have not
checked the HEAD.
Let me define a simple GADT |F|,
-- a simple GADT
data F :: * -> * where F :: Int -> F ()
and a more or less trivial function |g| operating on it:
-- type checks
g :: F a -> a -> Int
g (F n) () = n
No problems up to here. But then let me just flip the parameters of |
g|---and call the resulting function |h|:
-- does not type check
h :: a -> F a -> Int
h () (F n) = n-- !!!
Now, this definition of h does not type check:
Couldn't match the rigid variable `a' against `()'
`a' is bound by the type signature for `h'
Expected type: a
Inferred type: ()
When checking the pattern: ()
In the definition of `h': h () (F n) = n
So, it seems that there's a left-to-right bias in type checking
functions over GADTs. I cannot imagine this being by design, for it
certainly seems possible to type check functions of this sort in a
conceptually unbiased fashion.
Anyone to shine a light on this?
TIA,
Stefan
--
Bias.lhs:
> {-# OPTIONS -fglasgow-exts #-}
> -- a simple GADT
> data F :: * -> * where F :: Int -> F ()
> -- type checks
> g :: F a -> a -> Int
> g (F n) () = n
> -- does not type check
> h :: a -> F a -> Int
> h () (F n) = n-- !!!
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Left-to-right bias in type checking GADT functions
Yes, it's quite deliberate. See 5.4 of
http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf
The alternative design choice is to reject both programs, but in Haskell
(because of laziness) the evaluation order is prescribed, so accepting
the former seems right.
Simon
| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED]
| On Behalf Of Stefan Holdermans
| Sent: 20 June 2006 08:53
| To: Glasgow Haskell Users
| Subject: Left-to-right bias in type checking GADT functions
|
| Hi all,
|
| I have to admit that I haven't checked if this is a known issue...
| The following is tested with both GHC 6.4.1 and 6.4.2; I have not
| checked the HEAD.
|
| Let me define a simple GADT |F|,
|
|-- a simple GADT
|data F :: * -> * where F :: Int -> F ()
|
| and a more or less trivial function |g| operating on it:
|
|-- type checks
|g :: F a -> a -> Int
|g (F n) () = n
|
| No problems up to here. But then let me just flip the parameters of |
| g|---and call the resulting function |h|:
|
|-- does not type check
|h :: a -> F a -> Int
|h () (F n) = n-- !!!
|
| Now, this definition of h does not type check:
|
|Couldn't match the rigid variable `a' against `()'
| `a' is bound by the type signature for `h'
| Expected type: a
| Inferred type: ()
|When checking the pattern: ()
|In the definition of `h': h () (F n) = n
|
| So, it seems that there's a left-to-right bias in type checking
| functions over GADTs. I cannot imagine this being by design, for it
| certainly seems possible to type check functions of this sort in a
| conceptually unbiased fashion.
|
| Anyone to shine a light on this?
|
| TIA,
|
|Stefan
|
|
| --
|
| Bias.lhs:
|
| > {-# OPTIONS -fglasgow-exts #-}
|
| > -- a simple GADT
| > data F :: * -> * where F :: Int -> F ()
|
| > -- type checks
| > g :: F a -> a -> Int
| > g (F n) () = n
|
| > -- does not type check
| > h :: a -> F a -> Int
| > h () (F n) = n-- !!!
|
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Left-to-right bias in type checking GADT functions
Simon, Yes, it's quite deliberate. See 5.4 of http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf The alternative design choice is to reject both programs, but in Haskell (because of laziness) the evaluation order is prescribed, so accepting the former seems right. Yes, I've read it now and your point is clear. Thank you. Regards, Stefan ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
FFI: number of worker threads?
Hello, The paper "Extending the Haskell FFI with Concurrency" mentioned the following in Section 6.3: "GHC's run-time system employs one OS thread for every bound thread; additionally, there is a variable number of so-called "worker" OS threads that are used to execute the unbounded (lightweight) threads." How does the runtime system determine the number of worker threads? Is the number hardcoded in the RTS or dynamically adjustable? Can a programmer specify it as an RTS option or change it using an API? I would like to use a large number (say, 2000) of unbounded threads, each calling a blocking, safe foreign function via FFI import. What is supposed to happen if all the worker threads are used up? I tried this in the recent GHC 6.5 and got some kind of "runaway worker threads?" RTS failure message when more than 32 threads are used. Is it a current limitation of the RTS, or should I file a bug report for it? Thanks, Peng ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: FFI: number of worker threads?
I have a related question. The docs state that in some environments O/S threads are used when the -threaded flag is used with ghc, and non-O/S threads are used otherwise (presumably these are non-preemptive). Does this apply as well to the worker threads that are the subject of this email? On Tue, 20 Jun 2006 22:57:17 -0400 "Li, Peng" <[EMAIL PROTECTED]> wrote: > Hello, > > The paper "Extending the Haskell FFI with Concurrency" mentioned the > following in Section 6.3: > > "GHC's run-time system employs one OS thread for every bound thread; > additionally, there is a variable number of so-called "worker" OS > threads that are used to execute the unbounded (lightweight) threads." > > How does the runtime system determine the number of worker threads? > Is the number hardcoded in the RTS or dynamically adjustable? Can a > programmer specify it as an RTS option or change it using an API? > > I would like to use a large number (say, 2000) of unbounded threads, > each calling a blocking, safe foreign function via FFI import. What > is supposed to happen if all the worker threads are used up? I tried > this in the recent GHC 6.5 and got some kind of "runaway worker > threads?" RTS failure message when more than 32 threads are used. Is > it a current limitation of the RTS, or should I file a bug report for > it? > > Thanks, > Peng > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: FFI: number of worker threads?
Another related question. I have some threaded applications running which are servers and run continuously. A thread is spawned for each new connection, and the thread exits when the client terminates. I've noticed that the thread ID increases. On one process I checked today I am up to thread number 3300. The number of running threads is not increasing; only six threads are running on this particular process. The threads are cleaned up and exit. The thread _ID_ is continually increasing. Is this going to cause a problem when the thread ID exceeds some value? Do I have to force the server process to recycle periodically? These processes are designed to run continuously, and are running in a fairly demanding commercial environment for extended periods of time. They have proven to be very stable and reliable. I'm hopeful that it will not be necessary to recycle to force the thread ID to restart. Seth On Tue, 20 Jun 2006 22:57:17 -0400 "Li, Peng" <[EMAIL PROTECTED]> wrote: > Hello, > > The paper "Extending the Haskell FFI with Concurrency" mentioned the > following in Section 6.3: > > "GHC's run-time system employs one OS thread for every bound thread; > additionally, there is a variable number of so-called "worker" OS > threads that are used to execute the unbounded (lightweight) threads." > > How does the runtime system determine the number of worker threads? > Is the number hardcoded in the RTS or dynamically adjustable? Can a > programmer specify it as an RTS option or change it using an API? > > I would like to use a large number (say, 2000) of unbounded threads, > each calling a blocking, safe foreign function via FFI import. What > is supposed to happen if all the worker threads are used up? I tried > this in the recent GHC 6.5 and got some kind of "runaway worker > threads?" RTS failure message when more than 32 threads are used. Is > it a current limitation of the RTS, or should I file a bug report for > it? > > Thanks, > Peng > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re[2]: FFI: number of worker threads?
Hello Seth, Wednesday, June 21, 2006, 7:18:48 AM, you wrote: Seth and Li, look at http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/rts-libs/multi-thread.html it may answer some of your questions (page http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/ contains commentaries about GHC internals) > I have a related question. The docs state that in some >> The paper "Extending the Haskell FFI with Concurrency" mentioned the -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
