Re[2]: [Haskell-cafe] request for co-development: improving Data.CharEncoding module
Hello Shannon, Friday, May 26, 2006, 10:45:38 PM, you wrote: >> about it :) ). one of it's current drawbacks is lack of support for >> file encodings other than UTF-8 and Latin-1. if someone can work on > I wonder if it helps any to "steal" this code from Python and > translate it into Haskell. no. the algorithm is not complex, it just need to be programmed according to scheme i described -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: help with MPTC for type proofs?
David Roundy wrote:
class Commutable a b d c
commute :: Commutable a b d c =>
(Patch a b, Patch b c) -> (Patch a d, Patch d c)
But for this to work properly, I'd need to guarantee that
1. if (Commutable a b d c) then (Commutable a d b c)
2. for a given three types (a b c) there exists at most one type d
such that (Commutable a b c d)
The problem seems easily solvable, exactly as described. We need to
take care of the two requirements separately.
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module D1 where
data Patch a b = Patch String deriving Show
-- This is identical to what Tom Schrijvers wrote
class Commutable a b c d |
a b c -> d, -- 2.
a d c -> b -- based on 1. + 2.
-- But how do we make sure that Commutable a d c b exists whenever
-- Commutable a b c d does? very easily: with the help of another
-- type class
instance (Commutable' a b c d, Commutable' a d c b)
=> Commutable a b c d
I had not thought of using a double constraint. Very clever.
Why not also put this constraint in the class declaration? You don't want
any other instances of Commutable (or do you?):
class (Commutable' a b c d, Commutable' a d c b)
=> Commutable a b c d |
a b c -> d, -- 2.
a d c -> b -- based on 1. + 2.
Cheers,
Tom
--
Tom Schrijvers
Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium
tel: +32 16 327544
e-mail: [EMAIL PROTECTED]
Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: help with MPTC for type proofs?
On Fri, May 26, 2006 at 08:39:28PM -0700, [EMAIL PROTECTED] wrote: > > David Roundy wrote: > > class Commutable a b d c > > > > commute :: Commutable a b d c => > > (Patch a b, Patch b c) -> (Patch a d, Patch d c) > > > > But for this to work properly, I'd need to guarantee that > > > > 1. if (Commutable a b d c) then (Commutable a d b c) > > > > 2. for a given three types (a b c) there exists at most one type d > > such that (Commutable a b c d) > > The problem seems easily solvable, exactly as described. We need to > take care of the two requirements separately. I guess what hasn't been addressed is the question I didn't know to ask... I want the return type "d" to be a phantom type of some sort (although I'm not clear on the distinction between phantom and existential types). Ordinarily I'd do this with a GADT, which gives me a type that can't match any other. This at least is "safe", but what I want is to relax this constraint. So I'd like to return an existential type which contains the constraint enforces this class. (And I think I'm expressing this very poorly!) In short, I don't want to have to explicitely list which phantom types commute, since the "a b" in Patch a b *will* be phantom, existential types, so (as you say below) we can't list these instances explicitely: > > instance Commutable' PL1 PL2 PL3 PL2I > > -- If the latter is commented out, there will be an error in testab below > > instance Commutable' PL1 PL2I PL3 PL2 > However, something tells me that the above approach isn't useful. We > really would like to have as many patch labels as _dynamically_ > needed. Also, we probably would like to specify which patches commute > dynamically, rather than statically. That is, we wish to examine the > patches and only then conclude if they commute. Thus we need to > program with evidence. The function commute becomes a semantic > function: it really does something, at run-time. It examines the > patches. If it decides the patches commute, it produces the pair of > patches, marked with a unique and unforgeable type d -- along with the > evidence that d is indeed determined by b, and vice versa. We need > this evidence for the creative mixing of patches, as in the original > test. This approach is not unlike the one described half a year ago, > in response to a similar query: Indeed, we definitely need to determine commutation dynamically, but I'd like once that has been determined to be able to use the results statically (see below). > http://www.haskell.org/pipermail/haskell-cafe/2005-December/012703.html > > I still don't know if the were some problems with that > approach. Anyway, here's the complete code: I remember that email. I ended up discarding the idea, when I realized that the problem could be solved much more elegantly using GADTs as a type witness (with unsafeCoerce#, admittedly), so that I don't need to explicitely cast types. I'm hoping that if we can come up with a static solution to this (new) problem, I can again use GADTs to convert the static solution to a dynamic one. (Sorry if I'm being unclear... I suppose that's why I need to ask for help, since I'm not sure what's possible or if possible how it'd be done...) -- David Roundy http://www.darcs.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: help with MPTC for type proofs?
Can someone explain to me why this doesn't work?
> {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
> module MPTC where
>
> class C a b c d | a b c -> d, a d c -> b
>
> instance (C a b c d) => C a d c b
>
> data P a b = P deriving (Show)
>
> data CommuteResult a b c where
> CR :: C a b c d => (P a d, P d c) -> CommuteResult a b c
>
> commute :: (P a b, P b c) -> CommuteResult a b c
> commute (P, P) = CR (P, P)
>
> test (x,y) = do CR (y',x') <- return $ commute (x,y)
> CR (y'', x'') <- return $ commute (x,y)
> CR (x''',y''') <- return $ commute (y',x'')
> return ()
By my logic, it seems that if
x :: P a b
y :: P b c
then y' and x'' must have types
y' :: C a b c d => P a d
x'' :: C a b c e => P e c
but the functional dependencies of C tell us that e and d must be the same
type, so the code should typecheck (which it doesn't)!
I'm thinking that either the functional dependency constraint is weaker
than I thought, or that somehow GADTs aren't interacting with FDs as I'd
like, but I'm not sure which. Or, of course, it may be that my recursive
instance is not doing what I like. Or I may be just plain confused, as is
pretty clearly the case...
--
David Roundy
http://www.darcs.net
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Haskell RPC
Hello Joel, > I wish Glasgow Distributed Haskell (GdH) was more active and visible! are you've seen http://www.informatik.uni-kiel.de/~fhu/PUBLICATIONS/1999/ifl.ps.gz ? afair, source code was also available -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: help with MPTC for type proofs?
> I'm thinking that either the functional dependency constraint is weaker > than I thought, or that somehow GADTs aren't interacting with FDs as I'd > like, but I'm not sure which. Or, of course, it may be that my recursive > instance is not doing what I like. Or I may be just plain confused, as is > pretty clearly the case... The interaction between FD and GADTs is not very good, in our experience. Hopefully this will be fixed at some point. But in the mean time, what we ended up doing is to use GADTs instead of classes and FDs: data Eq a b where refl_eq :: Eq a a data Commute a b c d where -- Lemma that says that D is uniquely defined by A, B, and C. Comm_unique :: Commute a b c d -> Commute a b c d' -> Eq d d' -- Proof. Comm_unique p1 p2 = ... The problem is that in your case it seems that you do not want to explain to the type checker how D depends on A B C: you just want to say that it's uniquely defined. But maybe you can get away with: data Eq a b where refl_eq :: Eq a a data Commute a b c d -- No axioms provided to Haskell. -- Lemma that says that D is uniquely defined by A, B, and C. Comm_unique :: Commute a b c d -> Commute a b c d' -> Eq d d' -- The proof is not given either. Comm_unique p1 p2 = undefined When you'll do a case on "Comm_unique a b" (which will tell the type checker that D and D' are one and the same) you'll just want to make sure that Haskell doesn't try to look at the `refl_eq' value. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Linking to third party libraries in windows
That's an interesting statement that bears further scrutiny. I've been viewing monads as a kind of encapsulation in a quasi-hidden world state. Yes a monad is a function that would give you an output if you had access to the input world. That is the picture drawn in Simon Peyton Jones' tutorial. I've been thinking of actions in terms of the functions x -> IO(a), but Simon calls these IO actions and calls monads actions as you do. Is it your claim that whenever an 'IO action' is performed on something like IO (x) with x <- newListArray a l that the newListArray function will be called ? So with the old paradigm, where Rmatrix was stored as (Int, Int, IO(StorableArry Int CDouble)). A typical matrix operation, that calls out to a BLAS C routine cside_effect() looks something like this under the old scheme matfunc A = (u,v, arr) where u = f1 (getrows A) (getcols B) v = f2 (getrows A) (getcols B) arr = do arrA <- getarr A withStorableArray arrA (\vara -> cside_effect vara ) return arrA Now when one uses this code do A <- getAfromSomewhere fA = matfunc A B <- anotherfunc A fA has been changed by the cside_effect function, but A has not! Is it your contention that the array in A is essentially copied or created anew for every getarr A call? I think getarr A looked something like getarr (Rmatrix (r,c,arr)) = arr in the old technique, but now looks like getarr (Rmatrix (r,c,arr)) = return arr Is this perhaps an effect of lazy evaluation? When does one actually need to evaluate the constructor for the storable array contained in A? Hmmm. Is it that the rules specify that an IO action forces the evaluation of the value in the monad, but otherwise this value may be unevaluated? Soreturn x doesn't evaluate x but (return x) >>= \z -> IOfunc z does? This would actually make sense in the end. The IO action of A <- getAfromSomewhere would not evaluate the monad that is the third element of the tuple A, since there is no real 'need' to do so. So in fact no constructor of A's array would ever get evaluated until a function was applied to it, which would have to be in the form of an IO action. That's a nice mind twister. Clean's uniqueness types are a little easier to grasp I think. Ahh I think I understand now. It has to work that way or else you cannot guarantee the sequential execution property of monads. Thus if y :: IO (a) and you evaluate z <- func (f1 y) (f2 y), the evaluation order of y is controlled by what is implemented in func (and f1 and f2), not by evaluation rules for arguments. The value wrapped in y MUST remain unevaluated until IO 'actions' are performed on it. Brian Hulley wrote: this is not correct. IO (StorableArray Int CDouble) is a monadic *value* itself, which represents an *action* which returns a storable array, and since you are filling in the slot in Rmatrix with the action (newListArray a l), this monadic value represents the action of creating a new array whenever the action is executed. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Projects related to Haskell
I was just wondering, when the HCAR will come out. just the same, for people like me who are not very involved with the community, it is difficult to get an overview of the ongoing projects. the wiki says Gofer is now abandoned and Hugs replaces it. nice to know. I wonder how about Mondrian, Eden and the rest. there should be a mechanism to officially deprecate a project, shouldn't there? and once again, a mechanism to nominate a successor so that newbies like me will know where to start exploring. cheers. Imam __ Do You Yahoo!? Tired of spam? Yahoo! Mail has the best spam protection around http://mail.yahoo.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Linking to third party libraries in windows
Matthew Bromberg wrote: That's an interesting statement that bears further scrutiny. I've been viewing monads as a kind of encapsulation in a quasi-hidden world state. The IO monad can be viewed as encapsulating a function from a world state to a pair consisting of an updated world state and a "return value" as follows: data IO a = IO (RealWorld -> (RealWorld, a)) Yes a monad is a function that would give you an output if you had access to the input world. That is the picture drawn in Simon Peyton Jones' tutorial. I've been thinking of actions in terms of the functions x -> IO(a), but Simon calls these IO actions and calls monads actions as you do. So the function is contained *inside* the representation of the IO action so it's IO (x -> (x,a)) not x -> IO a Is it your claim that whenever an 'IO action' is performed on something like IO (x) with x <- newListArray a l that the newListArray function will be called ? If I write: do let n = newListArray a l p <- n q <- n two separate arrays will be created, because n is the action of creating a new array, and this action is executed twice in the body of the do. However, if I instead wrote: do x <- newListArray a l let r = return x p <- r q <- r only one array would be created, and this would be shared between x, p, and q, because the action (newListArray a l) is now only executed once (x is the result of the action ie the array, not the action itself) So with the old paradigm, where Rmatrix was stored as (Int, Int, IO(StorableArry Int CDouble)). A typical matrix operation, that calls out to a BLAS C routine cside_effect() looks something like this under the old scheme matfunc A = (u,v, arr) where u = f1 (getrows A) (getcols B) v = f2 (getrows A) (getcols B) arr = do arrA <- getarr A withStorableArray arrA (\vara -> cside_effect vara ) return arrA Now when one uses this code do A <- getAfromSomewhere fA = matfunc A B <- anotherfunc A fA has been changed by the cside_effect function, but A has not! Is it your contention that the array in A is essentially copied or created anew for every getarr A call? matfunc A never actually calls getarr A. It just sets up a tuple where the 3rd element is an IO action that, when that 3rd element is actually executed, would execute the 3rd element of the original A, and pass the array that was returned by it to your C function, and then return that array. I think the essence of the confusion is that there are two kinds of actions that the 3rd element of A might be bound to: 1) An action which just returns an array that was previously created 2) An action which creates a new array and returns that And both of these have the same type!!! because all the type system knows is that these two actions "do something (maybe nothing) then return an array" Case 2 was what you were doing right at the beginning, when the 3rd element was (newListArray a l), and case 1 was what I pointed out you could have used ie using the action (return arr) where arr was allocated during the construction of Rmatrix. I think getarr A looked something like getarr (Rmatrix (r,c,arr)) = arr in the old technique, but now looks like getarr (Rmatrix (r,c,arr)) = return arr Is this perhaps an effect of lazy evaluation? When does one actually need to evaluate the constructor for the storable array contained in A? Hmmm. Is it that the rules specify that an IO action forces the evaluation of the value in the monad, but otherwise this value may be unevaluated? No. An action, when executed, returns a value, but this doesn't imply that all actions have values stored in them. Bulat's illustration of getChar is a perfect example of this, since getChar has type IO Char but does not store the Char inside it, and executing it multiple times will in general give different characters back depending on your input stream... However the action (return 'q') also has type IO Char but this time, the 'q' is stored inside the action (return 'q'). So it matters exactly what action it is, since they can't be distinguished just by looking at the types. Soreturn x doesn't evaluate x but (return x) >> = \z -> IOfunc z does? If you executed (return x), what first happens is that the *function* return:: a-> IO a is applied to its argument value 'x' to get an *action* which, when executed, will be able to supply the result value x, then this action *is* executed, and x is available as the result. Depending on the particular monad, x may or may not be evaluated. AFAIK for the IO monad, it would not be, but I think it is possible to conceive of a monad where the return function would need to evaluate its argument. Also, even if x was unevaluated by it's journey through the return function and executed action which hands it onto the input of iofunc, iofunc may or may not evaluate it.
Re: [Haskell-cafe] Linking to third party libraries in windows
Brian Hulley wrote: If I write: do let n = newListArray a l p <- n q <- n two separate arrays will be created, because n is the action of creating a new array, and this action is executed twice in the body of the do. However, if I instead wrote: do x <- newListArray a l let r = return x p <- r q <- r I should have used the word "executed" instead of "write" and "wrote". Regards, Brian. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re[2]: [Haskell-cafe] Re: [Haskell] installing streams library
At Thu, 25 May 2006 13:42:11 +0400,
Bulat Ziganshin wrote:
>
> Hello Jeremy,
>
> Monday, May 22, 2006, 12:20:54 AM, you wrote:
>
> > For my own needs, I cabalized and debianized the Streams library. It
> > generates binary debs for ghc6 and hugs -- but I think the hugs
> > version is broken. In any case, it is a start, you can download the
> > packaging at:
>
> > http://www.n-heptane.com/nhlab/tmp/Streams_packaging.tar.gz
>
> can i include your work in the library itself?
Absolutely.
> is it better to include 'debian' directory to my archive or left
> this to the debian packagers?
If someone volunteers to maintain the package -- then it is probably
better to not keep a copy of the debian directory in your archive --
because it will often be out of date and confuse people -- and debian
users will be able to get the debianized source easily by typing,
'apt-get source haskell-streams'.
On the other hand -- if there is no one officially maintaing it -- it
would be useful to provide the debian directory (with a disclaimer) so
that debian users can easily build and install the .deb, since
subverting the debian package system tends to lead to long-term
complications.
> can you say how you are use my library? it's both interesting for me
> and can be helpful in deciding how it should be further developed
I am using it to serialize/deserialize haskell data structures so I
can store them in a Berkeley database.
To get them into BDB I need to convert the haskell data structure into
a C structure that looks like this:
struct __db_dbt {
void *data; /* Key/data */
u_int32_t size; /* key/data length */
};
Currently I am doing it like this -- but this will clearly fail if the
serialized data structure is longer than 512 bytes...
withDBT :: (Binary a) => a -> (Ptr DBT -> IO b) -> IO b
withDBT thedata f =
allocaBytes #{size DBT} $ \dbtPtr ->
allocaBytes 512 $ \dataPtr ->
do h <- openMemBuf dataPtr 512
withByteAlignedLE h $ flip put_ thedata
wrote <- vTell h
vClose h
#{poke DBT, data} dbtPtr (castPtr dataPtr)
#{poke DBT, size} dbtPtr ((fromIntegral wrote) :: Int)
f dbtPtr
I don't really need the file-system interface for this project -- what
would be nice is something like 'withCStringLen' and 'peekCString' for
the encode/decode functions:
type PtrLen a = (Ptr a, Int)
encodePtrLen :: (Binary a) => a -> (PtrLen a -> IO b) -> IO b
decodePtr :: (Binary a) => Ptr a -> IO a
I could simulate this by using 'encode' to convert the data structure
to a String and then use 'withCStringLen' to get the pointer and
length -- but having the intermediate String seems like it could be a
big performance hit.
Two alternative ideas are:
(1) accurately pre-calculate the size of the serialized structure and
allocate the correct amount of memory from the start
(2) start with a 'guess' and realloc the memory if the initial guess
is too small.
Both of those alternatives have their own problems -- so I think only
testing will tell what works best...
I have not looked at the library exhaustively, so if there is already
a good way to do this, let me know.
Thanks!
j.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Linking to third party libraries in windows
Hello Brian, Sunday, May 28, 2006, 1:06:06 AM, you wrote: > how best to understand IO but certainly before trying to do so, a state > monad is *infinitely* easier to understand and then provides a good basis > for understanding IO) > The first monad I understood was the state monad on page 261 of Paul Hudak's i can also point to paper: http://research.microsoft.com/users/simonpj/Papers/state-lasc.ps.gz and it's reduced variant: http://research.microsoft.com/users/simonpj/Papers/lazy-functional-state-threads.ps.Z there's also well-known http://www.nomaware.com/monads/monad_tutorial.zip -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
