Re: [Haskell] Should the following program be accepted by ghc?
stefanor: > On Wed, Jan 16, 2008 at 01:02:43PM +0800, Martin Sulzmann wrote: > > Bruno Oliveira writes: > > > I have been playing with ghc6.8.1 and type families and the following > > > program is accepted without any type-checking error: > > > > > > > data a :=: b where > > > >Eq :: a :=: a > ... > > > Ofcourse, that before ghc6.8, we add no type-level functions so maybe it > > > was ok to consider the program above. > ... > > > > type family K a > > Type families are unsupported, and their intersection with GADTs are > unimplemented. Don't expect any program which uses both to do anything > sane until 6.10. That being said, bug reports against the head version of GHC *are* welcome. But they're not an official feature of ghc 6.8, as Stefan hinted. -- Don ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Should the following program be accepted by ghc?
On Wed, Jan 16, 2008 at 01:02:43PM +0800, Martin Sulzmann wrote: > Bruno Oliveira writes: > > I have been playing with ghc6.8.1 and type families and the following > > program is accepted without any type-checking error: > > > > > data a :=: b where > > >Eq :: a :=: a ... > > Ofcourse, that before ghc6.8, we add no type-level functions so maybe it > > was ok to consider the program above. ... > > > type family K a Type families are unsupported, and their intersection with GADTs are unimplemented. Don't expect any program which uses both to do anything sane until 6.10. Stefan signature.asc Description: Digital signature ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Should the following program be accepted by ghc?
[Whoever replies next pl move discussion to haskell-cafe]
Bruno Oliveira writes:
> Hello,
>
> I have been playing with ghc6.8.1 and type families and the following
> program is accepted without any type-checking error:
>
> > data a :=: b where
> >Eq :: a :=: a
>
> > decomp :: f a :=: f b -> a :=: b
> > decomp Eq = Eq
>
> However, I find this odd because if you interpret "f" as a function and
> ":=:" as equality, then this is saying that
>
> if f a = f b then a = b
>
> but clearly this does not hold in general. For example:
>
> f 1 = 0
> f 2 = 0
>
> So, we have that "f 1 = f 2" but this does not imply that "1 = 2".
>
> Ofcourse, that before ghc6.8, we add no type-level functions so maybe it
> was ok to consider the program above.
Correct. The decomposition law
f a = f b ==> a = b
applies only to ordinary type constructors (eg list [] etc).
See the System FC paper for more details.
There's a (silent) constraint imposed on the program
> > decomp :: f a :=: f b -> a :=: b
> > decomp Eq = Eq
saying that f can only be instantiated with an ordinary type constructor.
As far as I know, GHC obeys this restriction (Manuel, Simon and Tom
who have implemented type families may be able to tell you more).
> However, with open type functions
> the following program is problematic and crashes ghc in style:
>
> > type family K a
>
> > c :: K a :=: K b -> a :=: b
> > c Eq = Eq
>
> with the following error message:
>
> ghc-6.8.1: panic! (the 'impossible' happened)
>(GHC version 6.8.1 for i386-apple-darwin):
> Coercion.splitCoercionKindOf
> base:GHC.Prim.sym{(w) tc 34v} co_aoW{tv} [tv]
> main:Bug.K{tc rom} a{tv aoS} [sk]
> ~
>main:Bug.K{tc rom} b{tv aoT} [sk]
>
> It seems to me that the "decomp" should be rejected in the first place?
> Maybe the fact that "decomp" is accepted is a bug in the compiler?
As said above, you are not allowed to instantiate f with a type family
constructor. Therefore, decomp is fine.
The above program text "crashes" becaue we canNOT deduce that
K a = K b ==> a =b
The decomposition law does NOT apply to type family constructors.
Indeed, ghc shouldn't crash here and instead provide a more helpful
error message.
Martin
> Any comments?
>
> Cheers,
>
> Bruno Oliveira
> ___
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] ANN: GLFW-0.3 released
GLFW is a Haskell module for GLFW OpenGL framework. It provides an alternative to GLUT for OpenGL based Haskell programs. The current 0.3 version is for download from hackageDB at: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/GLFW-0.3 Same as the previous 0.2 version it requires Cabal 1.2 or later for installation (which comes as default in GHC 6.8 or later). The installation is now conforming to the standard Cabal steps. New addition is the Haddock documentation for all interface functions. There is also a sample program to demonstrate its usage on the Haskell wiki site for GLFW: http://haskell.org/haskellwiki/GLFW Any feedbacks is welcome! I've only tested it on a limited number of platforms + GHC combinations, so if you have installation issue, please let me know. Thank you! -- Regards, Paul Liu Yale Haskell Group http://www.haskell.org/yale ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Should the following program be accepted by ghc?
Hello,
I have been playing with ghc6.8.1 and type families and the following
program is accepted without any type-checking error:
data a :=: b where
Eq :: a :=: a
decomp :: f a :=: f b -> a :=: b
decomp Eq = Eq
However, I find this odd because if you interpret "f" as a function and
":=:" as equality, then this is saying that
if f a = f b then a = b
but clearly this does not hold in general. For example:
f 1 = 0
f 2 = 0
So, we have that "f 1 = f 2" but this does not imply that "1 = 2".
Ofcourse, that before ghc6.8, we add no type-level functions so maybe it
was ok to consider the program above. However, with open type functions
the following program is problematic and crashes ghc in style:
type family K a
c :: K a :=: K b -> a :=: b
c Eq = Eq
with the following error message:
ghc-6.8.1: panic! (the 'impossible' happened)
(GHC version 6.8.1 for i386-apple-darwin):
Coercion.splitCoercionKindOf
base:GHC.Prim.sym{(w) tc 34v} co_aoW{tv} [tv]
main:Bug.K{tc rom} a{tv aoS} [sk]
~
main:Bug.K{tc rom} b{tv aoT} [sk]
It seems to me that the "decomp" should be rejected in the first place?
Maybe the fact that "decomp" is accepted is a bug in the compiler?
Any comments?
Cheers,
Bruno Oliveira
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
RE: [Haskell] Simulating client server communication with recursive monads
Thanks Chris, I appreciate your quick answer. Do you know what is the theoretical foundation for having mfix process side-effects in the lexical order as opposed to execution order? Could you point me to some papers, if you know of any off top your head? Thanks a lot, Jan -Original Message- From: Chris Kuklewicz [mailto:[EMAIL PROTECTED] Sent: Tuesday, January 15, 2008 11:07 AM To: Jan Stranik Cc: haskell Subject: Re: [Haskell] Simulating client server communication with recursive monads Jan Stranik wrote: > My question was why does the output from writer shows first all output > from server, then followed by all output from client. The effect of "mfix" is that the side-effects of the calculation still occur in the lexical order. Since server is before client, the output of the server precedes the client. > I would like to > see output from client and server to alternate in the order in which the > computation occurs, namely [server, client, server, client, server, > client, …]. Then you have to restructure the code slightly. This works: > import Control.Monad > > import Control.Monad.Writer.Lazy > > client:: [Integer] -> Writer [String] [Integer] > client as = do > dc <- doClient as > return (0:dc) > where > doClient (a:as) = do > tell ["Client " ++ show a] > as' <- doClient as > return ((a+1):as') > doClient [] = return [] > > server :: [Integer] -> Writer [String] [Integer] > server [] = return [] > server (a:as) = do > tell ["Server " ++ show a] > rs <- server as > return (2*a:rs) > > simulation :: [(String,String)] > simulation = > let (clientOut,clientLog) = runWriter (client serverOut) > (serverOut,serverLog) = runWriter (server clientOut) > in zip serverLog clientLog > > main = print (take 10 simulation) ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] hbeat: a rhythm sequencer
I've just uploaded to hackage a step-based music sequencer, called "hbeat". It's little more than a toy, but it's fun. It ought to be cross platform, though has been built and tested solely on linux. Given that it's only 400 or so lines, it may be a useful example for anyone wanting to combine OpenGL graphics, interaction, and sound via the SDL libraries. It's also interesting that more than half of the code is "pure" (ie outside the IO monad), despite the fact that this is a stateful app with real time interaction with the real world. Further details here: http://dockerz.net/software/hbeat.html Thanks to lemmih for the SDL bindings that made this possible. Tim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Simulating client server communication with recursive monads
Jan Stranik wrote: My question was why does the output from writer shows first all output from server, then followed by all output from client. The effect of "mfix" is that the side-effects of the calculation still occur in the lexical order. Since server is before client, the output of the server precedes the client. I would like to see output from client and server to alternate in the order in which the computation occurs, namely [server, client, server, client, server, client, …]. Then you have to restructure the code slightly. This works: import Control.Monad import Control.Monad.Writer.Lazy client:: [Integer] -> Writer [String] [Integer] client as = do dc <- doClient as return (0:dc) where doClient (a:as) = do tell ["Client " ++ show a] as' <- doClient as return ((a+1):as') doClient [] = return [] server :: [Integer] -> Writer [String] [Integer] server [] = return [] server (a:as) = do tell ["Server " ++ show a] rs <- server as return (2*a:rs) simulation :: [(String,String)] simulation = let (clientOut,clientLog) = runWriter (client serverOut) (serverOut,serverLog) = runWriter (server clientOut) in zip serverLog clientLog main = print (take 10 simulation) ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
RE: [Haskell] Simulating client server communication with recursive monads
John,
Your change makes just the server function to return the same number that it
receives. My server implementation multiplied the incoming number by two.
My question was why does the output from writer shows first all output from
server, then followed by all output from client. I would like to see output
from client and server to alternate in the order in which the computation
occurs, namely [server, client, server, client, server, client, .].
I know that for finite sequences, it is easily possible to reorder the
output from writer. However, it is not possible to reorder the output if the
sequence is infinite. That can be seen in my example program if it is
modified by removing the statement "take 10". In that case the program never
prints output from clients, the output printer will be only from the server.
Jan
From: John Vogel [mailto:[EMAIL PROTECTED]
Sent: Monday, January 14, 2008 8:33 PM
To: Jan Stranik
Cc: haskell@haskell.org
Subject: Re: [Haskell] Simulating client server communication with recursive
monads
If you redefine as follows:
server :: [Integer] -> Writer [String] [Integer]
server [] = return []
server (a:as) = do
tell ["Server " ++ show a]
rs <- server as
return (a:rs)
You get this for the output:
["Server 0","Server 1","Server 2","Server 3","Server 4","Server 5","Server
6","Server 7","Server 8","Server 9","Server 1
0","Client 0","Client 1","Client 2","Client 3","Client 4","Client 5","Client
6","Client 7","Client 8","Client 9"]
Then you just need to alternate the pattern. Though a real simulation of
sever traffic would account for the packets
not being recieved, rerequested, or recieved out of order. It also depends
whether you are simulating TCP or UDP.
On 1/14/08, Jan Stranik <[EMAIL PROTECTED]> wrote:
Hello,
I am trying to simulate a client server traffic using recursive lazy
evaluation. I am trying to do that in a recursive writer monad.
Following code is my attempt to simulate client server interaction and
collect its transcript:
{-# OPTIONS -fglasgow-exts #-}
module Main where
import Control.Monad.Writer.Lazy
simulation:: Writer [String] ()
simulation = mdo
a <- server cr
cr <- client $ take 10 a
return ()
server:: [Integer] -> Writer [String] [Integer]
server (a:as) = do
tell ["server " ++ show a]
rs <- server as
return ((a*2):rs)
server [] = return []
client:: [Integer] -> Writer [String] [Integer]
client as = do
dc <- doClient as
return (0:dc)
where
doClient (a:as) = do
tell ["Client " ++ show a]
as' <- doClient as
return ((a+1):as')
doClient [] = return []
main = return $ snd $ runWriter simulation
The problem that I see is that the transcript collected contains first all
output from the server, and then output from the client.
Here is an example of output that I see:
:["server 0","server 1","server 3","server 7","server 15","server
31","server 63","server 127","server 255","server 511","server 1023","Client
0","Client 2","Client 6","Client 14","Client 30","Client 62","Client
126","Client 254","Client 510","Client 1022"]
I would like to collect the output like:
:["client 0","server 0", "client 1",.]
This would allow me to remove the ending condition in simulation (take 10),
and instead rely fully on lazy evaluation to collect as many simulation
steps as needed by my computation.
I am still relatively new to the concepts of recursive monadic computations,
so I would appreciate any suggestions from experts on this mailing list.
Thank you
Jan
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] CMCS 2008: Extended deadline
[- Apologies for multiple copies -] DEADLINE EXTENSION: New deadline for submissions of regular papers on **Monday, January 21** CMCS 2008 9th International Workshop on Coalgebraic Methods in Computer Science http://www.cwi.nl/projects/cmcs08/ Budapest, Hungary April 4-6, 2008 Key Note Speaker: Dexter Kozen (to be confirmed) Invited Speakers: Stefan Milius and Dirk Pattinson Important Dates Extended deadline for submission of regular papers: January 21, 2008 Notification of acceptance of regular papers: February 11, 2008. Final version for the preliminary proceedings: February 18, 2008. Deadline for submission of short contributions: March 10, 2008. Notification of acceptance of short contributions: March 17, 2008. The workshop will be held in conjunction with the 11th European Joint Conferences on Theory and Practice of Software ETAPS 2008 March 29 - April 6, 2008 Programme Committee Jiri Adamek (chair, Braunschweig), Corina Cirstea (Southampton), Neil Ghani (Nottingham), H. Peter Gumm (Marburg), Bart Jacobs (Nijmegen), Clemens Kupke (co-chair, Amsterdam), Alexander Kurz (Leicester), Ugo Montanari (Pisa), Larry Moss (Indiana), John Power (Bath), Jan Rutten (Amsterdam), Lutz Schröder (Bremen), Tarmo Uustalu (Tallinn), Yde Venema (Amsterdam), Hiroshi Watanabe (Osaka). Submissions Two sorts of submissions will be possible this year: Papers to be evaluated by the programme committee for inclusion in the ENTCS proceedings: These papers must be written using ENTCS style files and be of length no greater than 20 pages. They must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. If a submission describes software, software tools, or their use, it should include all source code that is needed to reproduce the results but is not publicly available. If the additional material exceeds 5 MB, URL's of publicly available sites should be provided in the paper. Short contributions: These will not be published but will be compiled into a technical report of the Technical University of Braunschweig. They should be no more than two pages and may describe work in progress, summarise work submitted to a conference or workshop elsewhere, or in some other way appeal to the CMCS audience. Both sorts of submission should be submitted in postscript or pdf form as attachments to an email to [EMAIL PROTECTED] The email should include the title, corresponding author, and, for the first kind of submission, a text-only one-page abstract. After the workshop, we expect to produce a journal proceedings of extended versions of selected papers to appear in Theoretical Computer Science. For more information, please write to [EMAIL PROTECTED] ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] DEADLINE EXTENSION - SAS 2008
15th International Static Analysis Symposium - SAS 2008 Valencia, Spain - July 16-18 >>DEDLINE EXTENSION<< New important dates: Submission of abstract: January 19, 2008 (changed) Submission of full paper:January 26, 2008 (changed) Notification:March 7, 2008 Camera-ready version:April 5, 2008 Conference: July 16-18, 2008 Please see: http://www.dsic.upv.es/~sas2008/ Maria Alpuente, German Vidal (PC co-chairs) Email: [EMAIL PROTECTED] ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
