Re: [Haskell-cafe] threadWaitRead and threadWaitWrite on multiple fds

[Mathijs Kwik]

Yep, that's like the workaround I'm using right now.
I create an empty mvar, fire up 2 threads that will wait for an fd and
tryPutMVar afterwards.
My original thread justs gets the MVar to wait for any of the 2
fd-waiting-threads to complete.
But however light threads may be, I still think this might give some
overhead, and it's almost the same trick that System/Event/Thread is
using internally, although in that case, the putMVar is performed by
the event manager thread.
As far as I can tell, the behavior isn't hard-coded in the RTS (no
need to change that), but applications that use base will tell it to
use the mvar-trick as callback. That's why I was hoping to be able to
just tell it to use a different callback.

But indeed it's a solution for now.
I'll just post a feature-request for GHC.

Thanks


On Mon, Dec 13, 2010 at 3:19 AM, Mitar  wrote:
> Hi!
>
> On Mon, Dec 13, 2010 at 2:14 AM, Antoine Latter  wrote:
>> Can you do it with forkIO? That is, have two light-weight threads,
>> each waiting on a different fd, which perform the same action when one
>> of them wakes up.
>
> Or you could wait for each fd in its own thread (those are really
> light-weight threads) and once some is triggered you spawn another
> thread which deals with the event, while the original thread goes back
> into the waiting. Or you can also send data over Chan to another
> thread which then processes the even (if you need to serialize
> processing).
>
>
> Mitar
>

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] threadWaitRead and threadWaitWrite on multiple fds

[Johan Tibell]

On Mon, Dec 13, 2010 at 1:37 AM, Mathijs Kwik  wrote:
> Hi all,
>
> I read the paper about the new ghc7 event handling IO manager goodies.
> This is all very exciting stuff. I didn't know GHC's RTS had these
> smart async-IO facilities.
> The paper pointed me at threadWaitRead/threadWaitWrite.
> While very nice the way they are, I would also like to be able to wait
> on more than 1 fd until 1 of them becomes available.

You can fork a thread per fd and have the first thread that wakes up
kill the other threads using asynchronous exceptions. This is how e.g.
System.Timeout.timeout works.

Johan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] A home-brew iteration-alike library: some extension quiestions

[oleg]

Just for the record: the library IterateeM.hs, uses NO extensions to
Haskell98, let alone Haskell2010. The library as written requires
LowLevelIO.hs, which uses FFI (which has been Haskell98 addendum and
is in proper Haskell2010). The sample code, Wc.hs, for example, is
Haskell98. So, the iteratee can be written with no extensions
whatsoever.

In particular, IterateeM does not use any monad transformer library
(although it could have). I found that the trouble of writing a state
monad for a particular state is negligible compared to the pain of
choosing a particular monad transformer library, and especially the
pain inflicted on the users who have to deal with many a conflicts of
monad transformer libraries.


> The problem was that I wished Zippee. It means that external enumerator
> must be "suspended" at some points so Zippee can process elements from
> both left and right streams in desired order. It makes any other
> approach I considered impossible to use.

The file IterateeN.hs demonstrates zipping two streams together (in
lock-step and not in-lockstep). It turns out, the existing Iteratee
interface and type suffices. This is described in more detail in:

Parallel composition of iteratees: one source to several sinks
http://okmij.org/ftp/Streams.html#1enum2iter

Parallel composition of streams: several sources to one sink
http://okmij.org/ftp/Streams.html#2enum1iter


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] threadWaitRead and threadWaitWrite on multiple fds

[Mitar]

Hi!

On Mon, Dec 13, 2010 at 2:14 AM, Antoine Latter  wrote:
> Can you do it with forkIO? That is, have two light-weight threads,
> each waiting on a different fd, which perform the same action when one
> of them wakes up.

Or you could wait for each fd in its own thread (those are really
light-weight threads) and once some is triggered you spawn another
thread which deals with the event, while the original thread goes back
into the waiting. Or you can also send data over Chan to another
thread which then processes the even (if you need to serialize
processing).


Mitar

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] threadWaitRead and threadWaitWrite on multiple fds

[Antoine Latter]

On Sun, Dec 12, 2010 at 6:37 PM, Mathijs Kwik  wrote:
> Hi all,
>
> I read the paper about the new ghc7 event handling IO manager goodies.
> This is all very exciting stuff. I didn't know GHC's RTS had these
> smart async-IO facilities.
> The paper pointed me at threadWaitRead/threadWaitWrite.
> While very nice the way they are, I would also like to be able to wait
> on more than 1 fd until 1 of them becomes available.
>
> Would it be possible to create this functionality myself? Or do I need
> to request it and wait for a new GHC?
> It looks like the functionality I need is in System/Event/Thread.
> I think I can manage to write my own version of those functions which
> then loop through a list of fds, but the original file imports
> System/Event/Manager (registerFd, unregisterFd_) which I can't do
> because it's a hidden module.
> Is there a way around this?
>

Can you do it with forkIO? That is, have two light-weight threads,
each waiting on a different fd, which perform the same action when one
of them wakes up.

Maybe that would become too hard to synchronize the threads together,
but it might be the first thing to try before delving into GHC
internals.

Take care,
Antoine

>
> Thanks,
> Mathijs
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] threadWaitRead and threadWaitWrite on multiple fds

[Mathijs Kwik]

Hi all,

I read the paper about the new ghc7 event handling IO manager goodies.
This is all very exciting stuff. I didn't know GHC's RTS had these
smart async-IO facilities.
The paper pointed me at threadWaitRead/threadWaitWrite.
While very nice the way they are, I would also like to be able to wait
on more than 1 fd until 1 of them becomes available.

Would it be possible to create this functionality myself? Or do I need
to request it and wait for a new GHC?
It looks like the functionality I need is in System/Event/Thread.
I think I can manage to write my own version of those functions which
then loop through a list of fds, but the original file imports
System/Event/Manager (registerFd, unregisterFd_) which I can't do
because it's a hidden module.
Is there a way around this?


Thanks,
Mathijs

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Taking the TLS package for a spin ... and failing

[Mads Lindstrøm]

Hi again,

I found a simpler way to test the server connection, but it is still not
working. Namely,

> penssl s_client -connect 192.168.1.6:8000

> CONNECTED(0003)
> 18683:error:140790E5:SSL routines:SSL23_WRITE:ssl handshake > 
> failure:s23_lib.c:188:


Regards,

Mads Lindstrøm

On Sun, 2010-12-12 at 20:14 +0100, Mads Lindstrøm wrote:
> Hi Haskellers,
> 
> 
> I am trying to connect a Java client to a Haskell server using the
> Haskell tls package, and things are not working out for me. There is a
> lot of steps involved and I do not know what I am doing wrong, so this
> is a long message. But first I create a private/public key-pair:
> 
> > openssl genrsa -out privkey.pem 2048
> 
> then I make a self-signed certificate:
> 
> > openssl req -new -x509 -key privkey.pem -out cacert.pem -days 1095
> 
> > Country Name (2 letter code) [AU]:
> > State or Province Name (full name) [Some-State]:
> > Locality Name (eg, city) []:
> > Organization Name (eg, company) [Internet Widgits Pty Ltd]:
> > Organizational Unit Name (eg, section) []:
> > Common Name (eg, YOUR name) []:192.168.1.6
> > Email Address []:
> 
> then I convert the certificate to DER format and stuff it into a Java
> keystore:
> 
> > openssl x509 -in cacert.pem -out cert.der -outform DER
> > keytool -keystore myKeystore.store -importcert -storepass foobar -keypass 
> > foobar -file cert.der
> 
> now I start the Haskell server:
> 
> > ghc -hide-package monads-tf Server.hs -e main
> 
> and then the Java client:
> 
> > javac Client.java
> > java  -Djavax.net.debug=all -Djavax.net.ssl.trustStore=myKeystore.store 
> > -Djavax.net.ssl.trustStorePassword=foobar Client >JavaClientOutput.txt 2>&1
> 
> The server output is:
> 
> > : user error (unexpected type received. expecting handshake ++ 
> > Left (Error_Packet "invalid type"))
> 
> and not "Hello world" as expected.
> 
> The client output is very long, but the most interesting part is
> properly:
> 
> > main, received EOFException: error
> > main, handling exception: javax.net.ssl.SSLHandshakeException: Remote host 
> > closed connection during handshake
> > main, SEND TLSv1 ALERT:  fatal, description = handshake_failure
> 
> I have attached the Haskell server, the Java client and the full java
> output. Hope somebody can help figure out what I do wrong.
> 
> I am using the Haskell tsl package version 0.3.1. And I run Debian
> Linux.
> 
> 
> I also tried connecting a Java client to a Java server. First create
> server keystore:
> 
> > openssl pkcs8 -topk8 -nocrypt -in privkey.pem -inform PEM -out privkey.der 
> > -outform DER
> > java -Dkeystore=myServerKeystore.store ImportKey privkey.der cert.der
> 
> ImportKey.java can be found here
> http://www.agentbob.info/agentbob/79-AB.html .
> 
> then start Java server:
> 
> > javac JavaServer.java
> > java -Djavax.net.ssl.keyStore=myServerKeystore.store 
> > -Djavax.net.ssl.keyStorePassword=importkey JavaServer
> 
> and run the client again:
> 
> > java  -Djavax.net.debug=all -Djavax.net.ssl.trustStore=myKeystore.store 
> > -Djavax.net.ssl.trustStorePassword=foobar Client
> 
> and the server outputs:
> 
> > Hello world
> 
> as expected. Thus I think the certificates are fine, and the Java client
> is fine. But what am I doing wrong in the Haskell server?
> 
> I have attached JavaServer.java.
> 
> 
> Regards,
> 
> Mads Lindstrøm
> 


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Weird error during derive-2.3.0.2 build

[Alex]

Hi all.

I am trying to install the "yi" editor using cabal-install, which in turns
installs the package 'derive-2.3.0.2'. I get the following error during
derive's compilation:

[53 of 58] Compiling Data.Derive.Internal.Traversal (
Data/Derive/Internal/Traversal.hs,
dist/build/Data/Derive/Internal/Traversal.o )

Data/Derive/Internal/Traversal.hs:34:0:
Illegal instance declaration for `Applicative (Writer w)'
(All instance types must be of the form (T t1 ... tn)
 where T is not a synonym.
 Use -XTypeSynonymInstances if you want to disable this.)
In the instance declaration for `Applicative (Writer w)'
cabal: Error: some packages failed to install:
derive-2.3.0.2 failed during the building phase. The exception was:
ExitFailure 1

Of course, I tried to build it with --ghc-option=-XTypeSynonymInstances,
which in turn gives another compilation error.

I am using ubuntu maverick 32-bit, with ghc-6.12.1 and cabal-install 0.8.2.
The ghc was installed from the package repository. Cabal was installed
using:

cabal-install cabal

Alex.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] gtk2hs and hmake websites

[Duncan Coutts]

On 12 December 2010 20:55, Florian Weimer  wrote:

> So the net effect will be a migration from haskell.org to
> haskell.cs.yale.edu, and not to community.haskell.org.  I think that's
> pretty odd, but people will have their reasons for doing it this way.

I addition to what Thomas says, note that haskell.cs.yale.edu will be
shut down in approximately a month (there is a full filesystem backup
in case people have not moved things by then).

Duncan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] gtk2hs and hmake websites

[Thomas Schilling]

On 12 December 2010 20:55, Florian Weimer  wrote:
>
> * Joachim Breitner:
>
> > I get regular error message from some Debian tools that check for new
> > upstream versions that it cannot find http://haskell.org/hmake, and
> > http://haskell.org/gtk2hs seems to be gone as well since the recent move
> > of haskell.org. Is that temporary or will these projects have to find
> > new homes?
>
> There's a thread on the haskell list concerning this topic:
>
> 
>
> I just discovered this breakage while investigating the state of
> HaXml.  Without your message, I would have thought that HaXml is
> abandonware because all the links seem to be broken.  But then I
> discovered the discussion.
>
> In your case, the working links appear to be these:
>
> 
> 
>
> So the net effect will be a migration from haskell.org to
> haskell.cs.yale.edu, and not to community.haskell.org.  I think that's
> pretty odd, but people will have their reasons for doing it this way.

No, I think these websites just haven't been moved, yet.
haskell.cs.yale.edu was the location of haskell.org before the move
and the content is therefore still there.  Only haskell.org now points
to the new server which does not host these sites.  The policy for the
new server is different, so they won't be hosted directly on the new
server.  The correct new location will be community.haskell.org.

However, we can create redirects, so the old links will still work.
The procedure for the site maintainers is therefore the same as
mentioned in the thread you linked:

  1. Get an account on community.haskell.org
  2. Copy site content over.
  3. Ask for a redirect from haskell.org/ to
community.haskell.org/ at http://community.haskell.org/admin/

--
Push the envelope. Watch it bend.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] gtk2hs and hmake websites

[Florian Weimer]

* Joachim Breitner:

> I get regular error message from some Debian tools that check for new
> upstream versions that it cannot find http://haskell.org/hmake, and
> http://haskell.org/gtk2hs seems to be gone as well since the recent move
> of haskell.org. Is that temporary or will these projects have to find
> new homes?

There's a thread on the haskell list concerning this topic:



I just discovered this breakage while investigating the state of
HaXml.  Without your message, I would have thought that HaXml is
abandonware because all the links seem to be broken.  But then I
discovered the discussion.

In your case, the working links appear to be these:




So the net effect will be a migration from haskell.org to
haskell.cs.yale.edu, and not to community.haskell.org.  I think that's
pretty odd, but people will have their reasons for doing it this way.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] gtk2hs and hmake websites

[Joachim Breitner]

Hi,

I get regular error message from some Debian tools that check for new
upstream versions that it cannot find http://haskell.org/hmake, and
http://haskell.org/gtk2hs seems to be gone as well since the recent move
of haskell.org. Is that temporary or will these projects have to find
new homes?

Greetings,
Joachim

-- 
Joachim "nomeata" Breitner
  mail: m...@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C
  JID: nome...@joachim-breitner.de | http://www.joachim-breitner.de/
  Debian Developer: nome...@debian.org


signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] The Monad Reader links are broken

[Thomas Schilling]

I don't have access to the wordpress site, but here's a quick way to fix the
links:

 - Replace links of the form: 

 - With: 

/ Thomas

On 11 December 2010 23:28, Jason Dagit  wrote:
> Hello,
> I noticed today that the links in this article point to Haskell.org and
they
> are broken:
> http://themonadreader.wordpress.com/previous-issues/
> Maybe someone can fix this?
> Thanks!
> Jason



-- 
Push the envelope. Watch it bend.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Taking the TLS package for a spin ... and failing

[Mads Lindstrøm]

Hi Haskellers,


I am trying to connect a Java client to a Haskell server using the
Haskell tls package, and things are not working out for me. There is a
lot of steps involved and I do not know what I am doing wrong, so this
is a long message. But first I create a private/public key-pair:

> openssl genrsa -out privkey.pem 2048

then I make a self-signed certificate:

> openssl req -new -x509 -key privkey.pem -out cacert.pem -days 1095

> Country Name (2 letter code) [AU]:
> State or Province Name (full name) [Some-State]:
> Locality Name (eg, city) []:
> Organization Name (eg, company) [Internet Widgits Pty Ltd]:
> Organizational Unit Name (eg, section) []:
> Common Name (eg, YOUR name) []:192.168.1.6
> Email Address []:

then I convert the certificate to DER format and stuff it into a Java
keystore:

> openssl x509 -in cacert.pem -out cert.der -outform DER
> keytool -keystore myKeystore.store -importcert -storepass foobar -keypass 
> foobar -file cert.der

now I start the Haskell server:

> ghc -hide-package monads-tf Server.hs -e main

and then the Java client:

> javac Client.java
> java  -Djavax.net.debug=all -Djavax.net.ssl.trustStore=myKeystore.store 
> -Djavax.net.ssl.trustStorePassword=foobar Client >JavaClientOutput.txt 2>&1

The server output is:

> : user error (unexpected type received. expecting handshake ++ 
> Left (Error_Packet "invalid type"))

and not "Hello world" as expected.

The client output is very long, but the most interesting part is
properly:

> main, received EOFException: error
> main, handling exception: javax.net.ssl.SSLHandshakeException: Remote host 
> closed connection during handshake
> main, SEND TLSv1 ALERT:  fatal, description = handshake_failure

I have attached the Haskell server, the Java client and the full java
output. Hope somebody can help figure out what I do wrong.

I am using the Haskell tsl package version 0.3.1. And I run Debian
Linux.


I also tried connecting a Java client to a Java server. First create
server keystore:

> openssl pkcs8 -topk8 -nocrypt -in privkey.pem -inform PEM -out privkey.der 
> -outform DER
> java -Dkeystore=myServerKeystore.store ImportKey privkey.der cert.der

ImportKey.java can be found here
http://www.agentbob.info/agentbob/79-AB.html .

then start Java server:

> javac JavaServer.java
> java -Djavax.net.ssl.keyStore=myServerKeystore.store 
> -Djavax.net.ssl.keyStorePassword=importkey JavaServer

and run the client again:

> java  -Djavax.net.debug=all -Djavax.net.ssl.trustStore=myKeystore.store 
> -Djavax.net.ssl.trustStorePassword=foobar Client

and the server outputs:

> Hello world

as expected. Thus I think the certificates are fine, and the Java client
is fine. But what am I doing wrong in the Haskell server?

I have attached JavaServer.java.


Regards,

Mads Lindstrøm


import javax.net.*;
import java.net.*;
import javax.net.ssl.*;
import java.io.*;

class Client {
public static void main(String[] args) {
	try {
	int port = 8000;
	String hostname = "192.168.1.6";  // Insert your localhost ip
	SocketFactory socketFactory = SSLSocketFactory.getDefault();
	Socket socket = socketFactory.createSocket(hostname, port);
	// Create streams to securely send and receive data to the server
	InputStream in = socket.getInputStream();
	OutputStream out = socket.getOutputStream();
	
	PrintWriter writer = new PrintWriter(out);
	writer.println("Hello world");
	
	// Read from in and write to out...
	// Close the socket 
	writer.close();
	in.close(); 
	out.close();
	} catch(IOException e) {
	e.printStackTrace();
	System.out.println(e.getMessage());
	}
}
} 

import javax.net.*;
import java.net.*;
import javax.net.ssl.*;
import java.io.*;

class JavaServer {
public static void main(String[] args) {
	try {
	int port = 8000;
	String hostname = "192.168.1.6";  // Insert your localhost ip
	
	ServerSocketFactory ssocketFactory = SSLServerSocketFactory.getDefault();
	ServerSocket ssocket = ssocketFactory.createServerSocket(port); 
	
	// Listen for connections
	Socket socket = ssocket.accept();

	// Create streams to securely send and receive data to the client
	InputStream in = socket.getInputStream();
	OutputStream out = socket.getOutputStream(); 

	BufferedReader reader = new BufferedReader(new InputStreamReader(in));
	System.out.println(reader.readLine());
	
	// Read from in and write to out...
	// Close the socket 
	reader.close();
	in.close(); 
	out.close();
	} catch(IOException e) {
	e.printStackTrace();
	System.out.println(e.getMessage());
	}
}
} -- ghci -hide-package monads-tf Server.hs

module Main where

import qualified Control.Monad.Trans as Trans
import qualified Data.ByteString as B
import qualified Data.ByteString.Lazy as L
import qualified Data.Certificate.PEM as PEM
import qualified Data.Certificate.Key as Key
import qualified Data.Certificate.X509 as X509

impor

Re: [Haskell-cafe] Avoiding the Y combinator for self-referencing types

[Florian Weimer]

* Miguel Mitrofanov:

> Not sure if that's what you need:
>
> data NodeF f = Node {name :: String, refs :: [f (NodeF f)]}
>
> newtype Const a b = Const a
> newtype Id a = Id a
>
> type NodeS = NodeF (Const String)
> type Node = NodeF Id

Thanks for the suggestion.  Yes, the resulting syntax looks better,
and it is more obvious to me what is going on.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Avoiding the Y combinator for self-referencing types

[Miguel Mitrofanov]

Not sure if that's what you need:

data NodeF f = Node {name :: String, refs :: [f (NodeF f)]}

newtype Const a b = Const a
newtype Id a = Id a

type NodeS = NodeF (Const String)
type Node = NodeF Id

Отправлено с iPhone

Dec 12, 2010, в 20:54, Florian Weimer  написал(а):

> Suppose I've got some named objects which reference other objects by
> name:
> 
>> data NodeS = NodeS {nameS :: String, refsS :: [String]}
> 
> Through name resolution, the strings are translated to the actual
> nodes they denote:
> 
>> data Node = Node {name :: String, refs :: [Node]}
>> resolve :: [NodeS] -> Map String Node
> 
> NodeS and Node are quite similar, so they should probably be the same
> parametrized type.  However, if I turn the type of the references into
> a type parameter, I need the type-level Y combinator to avoid an
> infinite type, and manipulating nodes turns a bit more tedious because
> of increased syntactic overhead.
> 
> Is there a third choice, beyond manually expanding the type definition
> or using Y?
> 
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Avoiding the Y combinator for self-referencing types

[Florian Weimer]

Suppose I've got some named objects which reference other objects by
name:

> data NodeS = NodeS {nameS :: String, refsS :: [String]}

Through name resolution, the strings are translated to the actual
nodes they denote:

> data Node = Node {name :: String, refs :: [Node]}
> resolve :: [NodeS] -> Map String Node

NodeS and Node are quite similar, so they should probably be the same
parametrized type.  However, if I turn the type of the references into
a type parameter, I need the type-level Y combinator to avoid an
infinite type, and manipulating nodes turns a bit more tedious because
of increased syntactic overhead.

Is there a third choice, beyond manually expanding the type definition
or using Y?

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] ANN: improve-0.2.2

[Tom Hawkins]

ImProve [1] is an imperative DSL for high assurance, embedded
applications.  This release includes a new compositional proof
framework where users can leverage previously proved theorems to aid
the proof of new theorems.  This new addition was inspired from
discussions with Lee Pike [2].

Lee also recommended the strategy of building disjunctive invariants
to reduce, if not eliminate the need for multi step induction, thus
dramatically reducing proof time.  Using these new strategies with
ImProve, we where able to verify several realtime safety properties of
an Eaton Hybrid Hydraulic program.

-Tom

[1] http://hackage.haskell.org/package/improve
[2] 
http://groups.google.com/group/fp-embedded/browse_thread/thread/63cd023e8f17b613?hl=en

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Contexts for type family instances

[Stephen Tetley]

On 12 December 2010 13:03, Max Bolingbroke  wrote:

>
> type instance DUnit (a,b) = GuardEq (DUnit a) (DUnit b)
>
> type family GuardEq a b :: *
> type instance GuardEq a a = a


Thanks Max, that seems to be what I need.


Best wishes

Stephen

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Contexts for type family instances

[Max Bolingbroke]

On 12 December 2010 12:26, Stephen Tetley  wrote:
>> type instance (DUnit a ~ DUnit b) => DUnit (a,b)           = DUnit a

Requires UndecidableInstances but should work:

"""
{-# LANGUAGE TypeFamilies #-}

type family DUnit a :: *

data Point u = P2 u u
type instance DUnit (Point u) = u

type instance DUnit (a,b) = GuardEq (DUnit a) (DUnit b)

type family GuardEq a b :: *
type instance GuardEq a a = a
"""

More realistically, you will have to write functions that
produce/consume DUnit using type classes so you can pattern match on
the "a" of "DUnit a". You could just have all your instances for
"DUnit (a, b)" require (DUnit a ~ DUnit b):

"""
class Consume a where
  consume :: DUnit a -> Foo
instance (DUnit a ~ DUnit b) => Consume (a, b) where
  consume a = undefined
"""

Cheers,
Max

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Contexts for type family instances

[Stephen Tetley]

Hello all

I've a type family DUnit that I use to allow the unit type, usually a
Double, of geometric things (points, vectors...) to be parametric:

> type family DUnit a :: *

E.g for Points

> data Point u = P2 u u

> type instance (Point u) = u

I can make an type instance for Maybe like this, using DUnit on the
right hand side:

> type instance DUnit (Maybe a)   = DUnit a


But pair is a problem. Is there a way to assert both parts of a pair
should have the same DUnit?

The code below won't compile but it should illustrate what I'm trying to do.

> type instance (DUnit a ~ DUnit b) => DUnit (a,b)   = DUnit a

I don't want to pick an arbitrary side, e.g:

> type instance DUnit (a,b)   = DUnit a

or

> type instance DUnit (a,b)   = DUnit b



Thanks

Best wishes

Stephen

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How can i insert graphic into a haddock document?

[Poprádi Árpád]

Thank You!

Árpád

On Sat, 2010-12-11 at 17:32 +0100, David Waern wrote:
> 2010/12/11 Poprádi Árpád 
> >
> > Hi,
> >
> > I have found nothing about this topic in the haddock documentation.
> > Is there a light way to do that?
> 
> Yes:
> 
> -- | <>
> 
> The documentation should be updated.
> 
> David
> 




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe