Re: [Haskell-cafe] Statically tracking "validity" - suggestions?
On 31 aug 2010, at 08:24, strejon wrote:
>
> Hello. I'm using Haskell to write a specification for some software. The
> software uses certificates (standard X.509 certificates) and stores user
> name information in the Subject's CommonName field.
>
> The X.509 standard doesn't actually require the presence of a CommonName
> field so the contents of the Subject section (with the rest of the fields
> omitted) are just represented by a Maybe User_Name.
>
>> import Data.List (find, concat)
>> import Data.Maybe (fromJust, isJust)
>>
>> type User_Name= String
>> type Public_Key = Integer
>> data Subject_Name = Subject_Name (Maybe User_Name) deriving (Show, Eq)
>>
>> data Certificate = Certificate {
>> certificate_subject :: Subject_Name,
>> certificate_key :: Public_Key,
>> certificate_issuer :: String,
>> certificate_serial :: Integer
>> } deriving (Show, Eq)
>
> This is all well and good, but the problem is that the validity of
> certificates isn't tracked statically and I have to use the following
> as guards on all functions that only expect valid certificates (and
> inevitably handle cases that I know can't actually happen but
> have to be handled in pattern matching and the like, bloating
> the specification):
>
>> user_name :: Subject_Name -> Maybe User_Name
>> user_name (Subject_Name name) = name
>>
>> is_valid :: Certificate -> Bool
>> is_valid = isJust . user_name . certificate_subject
>
> I'm aware of phantom types and the like, but I've been unable to
> work out how to use them (or another type system extension)
> to properly track "validity" on the type level. I'd want something
> like:
>
> validate :: Certificate Possibly_Valid -> Maybe (Certificate Valid)
>
> With later functions only accepting values of type "Certificate Valid".
>
> Is there a simple way to do this?
Yes. Introduce a wrapper datatype, ValidCertificate. Create a module and export
only the wrapper datatype and a way to construct ValidCertificates in a safe
way:
> module ValidateCertificate
> ( ValidCertificate,
> fromValidCertificate,
> createValidCertificate
> ) where
>
> data ValidCertificate = ValidCertificate {fromValidCertificate :: Certificate}
>
> createValidCertificate :: Certificate -> Maybe ValidCertificate
> createValidCertificate c | is_valid c = Just (ValidCertificate c)
> | otherwise = Nothing
>
> is_valid :: Certificate -> Bool
> is_valid = isJust . user_name . certificate_subject
The trick is not to export the constructor, but only a verified way to
construct values of ValidCertificate.
-chris___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Statically tracking "validity" - suggestions?
Hello. I'm using Haskell to write a specification for some software. The
software uses certificates (standard X.509 certificates) and stores user
name information in the Subject's CommonName field.
The X.509 standard doesn't actually require the presence of a CommonName
field so the contents of the Subject section (with the rest of the fields
omitted) are just represented by a Maybe User_Name.
> import Data.List (find, concat)
> import Data.Maybe (fromJust, isJust)
>
> type User_Name= String
> type Public_Key = Integer
> data Subject_Name = Subject_Name (Maybe User_Name) deriving (Show, Eq)
>
> data Certificate = Certificate {
> certificate_subject :: Subject_Name,
> certificate_key :: Public_Key,
> certificate_issuer :: String,
> certificate_serial :: Integer
> } deriving (Show, Eq)
This is all well and good, but the problem is that the validity of
certificates isn't tracked statically and I have to use the following
as guards on all functions that only expect valid certificates (and
inevitably handle cases that I know can't actually happen but
have to be handled in pattern matching and the like, bloating
the specification):
> user_name :: Subject_Name -> Maybe User_Name
> user_name (Subject_Name name) = name
>
> is_valid :: Certificate -> Bool
> is_valid = isJust . user_name . certificate_subject
I'm aware of phantom types and the like, but I've been unable to
work out how to use them (or another type system extension)
to properly track "validity" on the type level. I'd want something
like:
validate :: Certificate Possibly_Valid -> Maybe (Certificate Valid)
With later functions only accepting values of type "Certificate Valid".
Is there a simple way to do this?
--
View this message in context:
http://old.nabble.com/Statically-tracking-%22validity%22---suggestions--tp29579872p29579872.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: combinators in the syb lib -- or generic heterogeneous traversals that fold
i'm sorry, the example with the flip list would be flipList [[1,2],[3,4]] ==[4,3,2,1] On Mon, Aug 30, 2010 at 10:54 PM, Carter Schonwald < carter.schonw...@gmail.com> wrote: > Hello All, > In the course of some code I've been working on, I found I needed generic > foldl / foldr over heterogeneous data structures, where I can easily pick > whether I want top down left right, botom up left right, and ___ right > left traversals, and to in tandem sensibly approach if a parent node should > be included altogether > > What i'm wondering is if i'm somehow overlooking some simpler ways of > writing such or if my attached code for the foldl case (the foldr analogue > is easy to see from the example code). > > code with example follows > > --- my "foldl" that is abstracted from traversal order > travL :: (b -> a -> b)-> > GenericQ (Maybe a) -> > (Maybe a -> b ->(b -> a -> b)->(b->b)-> b) -> > GenericQ (b ->b) > travL f qry merge x nil = merge (qry x) nil f (\nl-> > foldl (flip ($)) nl $ > gmapQ (travL f qry merge) x ) > > --travR could be written as > --- travR f qry merge x nil = foldl (flip f) nil $ travL (flip (:)) qry > merge x [] > > -- example usage > -- takes the integers in some datastructure, and puts them in a list > -- example: > flipList :: Data a => a -> [Integer] > flipList x = travL (flip (:) ) (mkQ Nothing (Just :: Integer -> Maybe > Integer) ) (\ v nl f k -> maybe (k nl) (\y -> k $! f nl y) v ) x [] > > > I suppose that i could simplify it to > > travL :: GenericQ (Maybe a) -> > (Maybe a -> b ->(b->b)-> b) -> > GenericQ (b ->b) > > and have the operand *f* of the fold work within the *merge* parameter, > but that doesn't address the important bit in my mind, > namely that while its pretty clear to me that I can write the *synthesize*and > *everything* combinators using my "travL/R" stuff, its not clear to me > that the converse or something close to it is the case. > > Anyways, what're everyone's thoughts? > thanks! > -Carter > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] combinators in the syb lib -- or generic heterogeneous traversals that fold
Hello All, In the course of some code I've been working on, I found I needed generic foldl / foldr over heterogeneous data structures, where I can easily pick whether I want top down left right, botom up left right, and ___ right left traversals, and to in tandem sensibly approach if a parent node should be included altogether What i'm wondering is if i'm somehow overlooking some simpler ways of writing such or if my attached code for the foldl case (the foldr analogue is easy to see from the example code). code with example follows --- my "foldl" that is abstracted from traversal order travL :: (b -> a -> b)-> GenericQ (Maybe a) -> (Maybe a -> b ->(b -> a -> b)->(b->b)-> b) -> GenericQ (b ->b) travL f qry merge x nil = merge (qry x) nil f (\nl-> foldl (flip ($)) nl $ gmapQ (travL f qry merge) x ) --travR could be written as --- travR f qry merge x nil = foldl (flip f) nil $ travL (flip (:)) qry merge x [] -- example usage -- takes the integers in some datastructure, and puts them in a list -- example: flipList :: Data a => a -> [Integer] flipList x = travL (flip (:) ) (mkQ Nothing (Just :: Integer -> Maybe Integer) ) (\ v nl f k -> maybe (k nl) (\y -> k $! f nl y) v ) x [] I suppose that i could simplify it to travL :: GenericQ (Maybe a) -> (Maybe a -> b ->(b->b)-> b) -> GenericQ (b ->b) and have the operand *f* of the fold work within the *merge* parameter, but that doesn't address the important bit in my mind, namely that while its pretty clear to me that I can write the *synthesize*and *everything* combinators using my "travL/R" stuff, its not clear to me that the converse or something close to it is the case. Anyways, what're everyone's thoughts? thanks! -Carter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quick Question for QuickCheck2
On 31 August 2010 03:18, Lyndon Maydwell wrote: > Thanks! > > This makes perfect sense, but as I just discovered using ghci -v there > is an even stranger problem. I'm side-tracking slightly from the > original question here, but nevertheless... > > GHC gives the following output: > > --- > GHCi, version 6.12.3: http://www.haskell.org/ghc/ :? for help > : cannot satisfy -package QuickCheck-2.1.1.1: > QuickCheck-2.1.1.1-c7435cb0d5b5de72fe9540c48335606d is unusable > due to missing or recursive dependencies: > ghc-6.12.3-66a382195c8a71849653439b67021fd1 > (use -v for more information) > > shell returned 1 What does "ghc-pkg check" say? To me, it sounds like you upgraded a boot library, which is a big no-no. (The ghc mentioned here is the ghc library, not the compiler itself.) -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Ed Lambda: Functional programming meetup in Edinburgh
Looks good! I shall try to make it along. I'll have just come from my SICP study group at that point so will want some statically typed chat to soothe the pain :-) D On Mon, Aug 30, 2010 at 9:00 PM, Ollie Saunders wrote: > Hi guys, > > I'm running a meetup for functional programming in Edinburgh. The > first one will be on the 13th of September at Malone's Irish Bar (14 > Forrest Road) and will continue every 2nd monday of each month. For > the first meetup I think we'll just be having a chat and getting to > know each other but I hope to be able to expand it to talks and coding > dojos once we have some regular numbers. > > For more details: http://meetup.com/ed-lambda/ > And we're on Twitter: http://twitter.com/ed_lambda > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Dougal Stanton dou...@dougalstanton.net // http://www.dougalstanton.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Ed Lambda: Functional programming meetup in Edinburgh
Hi guys, I'm running a meetup for functional programming in Edinburgh. The first one will be on the 13th of September at Malone's Irish Bar (14 Forrest Road) and will continue every 2nd monday of each month. For the first meetup I think we'll just be having a chat and getting to know each other but I hope to be able to expand it to talks and coding dojos once we have some regular numbers. For more details: http://meetup.com/ed-lambda/ And we're on Twitter: http://twitter.com/ed_lambda ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quick Question for QuickCheck2
Thanks! This makes perfect sense, but as I just discovered using ghci -v there is an even stranger problem. I'm side-tracking slightly from the original question here, but nevertheless... GHC gives the following output: --- GHCi, version 6.12.3: http://www.haskell.org/ghc/ :? for help : cannot satisfy -package QuickCheck-2.1.1.1: QuickCheck-2.1.1.1-c7435cb0d5b5de72fe9540c48335606d is unusable due to missing or recursive dependencies: ghc-6.12.3-66a382195c8a71849653439b67021fd1 (use -v for more information) shell returned 1 --- However I am using the version of GHC mentioned, so I have no idea what is going on. On Tue, Aug 31, 2010 at 1:09 AM, John Millikin wrote: > Update your cabal package list, and then install QuickCheck. > Optionally, you can use a version specifier: > > cabal update > cabal install 'QuickCheck >= 2' > > This should make QuickCheck 2 the default in GHCI. If it doesn't, you > may need to specify the version: > > ghci -package QuickCheck-2.2 > > For Cabal-packaged libraries/applications, simply update your version > requirements. > > > On Mon, Aug 30, 2010 at 09:06, Lyndon Maydwell wrote: >> I'm just trying these examples, and I can't figure out how to import >> quickcheck2 rather than quickcheck1. I've looked around but I can't >> seem to find any information on this. How do I do it? >> >> Thanks! > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quick Question for QuickCheck2
Update your cabal package list, and then install QuickCheck. Optionally, you can use a version specifier: cabal update cabal install 'QuickCheck >= 2' This should make QuickCheck 2 the default in GHCI. If it doesn't, you may need to specify the version: ghci -package QuickCheck-2.2 For Cabal-packaged libraries/applications, simply update your version requirements. On Mon, Aug 30, 2010 at 09:06, Lyndon Maydwell wrote: > I'm just trying these examples, and I can't figure out how to import > quickcheck2 rather than quickcheck1. I've looked around but I can't > seem to find any information on this. How do I do it? > > Thanks! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quick Question for QuickCheck2
I'm just trying these examples, and I can't figure out how to import quickcheck2 rather than quickcheck1. I've looked around but I can't seem to find any information on this. How do I do it? Thanks! On Mon, Aug 30, 2010 at 11:56 PM, John Millikin wrote: > Define a custom element generator, which has characters with your > desired values: > > myRange :: Gen Char > myRange = elements (['A'..'Z'] ++ ['a' .. 'z'] ++ " ~...@#$%^&*()") > > You can use "forAll" to run tests with a specific generator: > > forAll myRange $ \c -> chr (ord c) == c > > On Mon, Aug 30, 2010 at 08:12, Sebastian Höhn > wrote: >> Hello, >> >> perhaps I am just blind or is it a difficult issue: I would like to >> generate Char values in a given Range for QuickCheck2. There is this >> simple example from the haskell book: >> >> instance Arbitrary Char where >> arbitrary = elements (['A'..'Z'] ++ ['a' .. 'z'] ++ " ~...@#$%^&*()") >> >> This does not work in QuickCheck2 since the instance is already >> defined. How do I achieve this behaviour in QC2? >> >> Thanks for helping. >> >> Sebastian >> ___ >> 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 mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quick Question for QuickCheck2
Define a custom element generator, which has characters with your desired values: myRange :: Gen Char myRange = elements (['A'..'Z'] ++ ['a' .. 'z'] ++ " ~...@#$%^&*()") You can use "forAll" to run tests with a specific generator: forAll myRange $ \c -> chr (ord c) == c On Mon, Aug 30, 2010 at 08:12, Sebastian Höhn wrote: > Hello, > > perhaps I am just blind or is it a difficult issue: I would like to > generate Char values in a given Range for QuickCheck2. There is this > simple example from the haskell book: > > instance Arbitrary Char where > arbitrary = elements (['A'..'Z'] ++ ['a' .. 'z'] ++ " ~...@#$%^&*()") > > This does not work in QuickCheck2 since the instance is already > defined. How do I achieve this behaviour in QC2? > > Thanks for helping. > > Sebastian > ___ > 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
Re: [Haskell-cafe] Re: Support for lock-free/wait-free programming? / ANN: bits-atomic
Gabriel Wicke writes: > On Sun, 29 Aug 2010 13:08:48 -0400, Gregory Collins wrote: > > After some more off-list discussion with Gregory (thanks for your help!) I > split out the atomic operations to the bits-atomic package [1] which no longer > depends on libgcc_s. GCC produces native code for atomic operations, so > libgcc_s is not needed for these operations. Wonderful, works perfectly, thanks! G -- Gregory Collins ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Hackage on Linux
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 On 8/30/10 06:26 , Andrew Coppin wrote: > Stephen Tetley wrote: >> \MinGW\include > > Isn't that "MinGW has a standard place for header files"? > > I'm guessing if you use DJGPP or MS VisualStudio or Borland C++, it's not > going to look there (unless you tell it to). Presumably that's what he meant by > Its a defacto standard, but its still a standard. If people are using > Cygwin or Microsoft's Unix compatibility layer, Visual C or even the > parts of MinGW distributed with GHC, they aren't documenting their > successes so no-one else can follow them, for all intents and purposes > MinGW/Msys is the only game in town. Again (echoing both the above and an earlier message of mine): if you can tell us(*) what to do to make things visible to VS, please do. Or contribute patches to Cabal that interoperate with VS. (*) generic "us"; I don't currently work on Cabal - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -BEGIN PGP SIGNATURE- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkx7zscACgkQIn7hlCsL25UKLwCfQwvnWnL5t7o55ZB8ZUq/IZhq ul0An0LoTBJQBIC3UVM+eZQcv5OfJ9K8 =sHJ2 -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quick Question for QuickCheck2
You can create a wrapper with a newtype and then define an instance for that. newtype Char2 = Char2 Char instance Arbitrary Char2 where arbitrary = ... You'll have to do some wrapping and unwrapping when calling your properties to get/set the underlying Char, but this is probably the easiest way to 'constrain' the possible arbitrary results when the default instance for Char can be "too much." On Mon, Aug 30, 2010 at 10:12 AM, Sebastian Höhn wrote: > Hello, > > perhaps I am just blind or is it a difficult issue: I would like to > generate Char values in a given Range for QuickCheck2. There is this > simple example from the haskell book: > > instance Arbitrary Char where > arbitrary = elements (['A'..'Z'] ++ ['a' .. 'z'] ++ " ~...@#$%^&*()") > > This does not work in QuickCheck2 since the instance is already > defined. How do I achieve this behaviour in QC2? > > Thanks for helping. > > Sebastian > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- - Austin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Partial Signatures with Implicit Parameters
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 On 8/30/10 09:21 , Alex Rozenshteyn wrote: > I would like to specify that a function takes implicit parameters, without > specifying its full return type. My main motivation for this is my xmonad > config file and the attempt to remove the need for NoMonomorphismRestriction > and some of the code smell associated with global variables that wafts in > with implicit parameters. > > I have read this: http://okmij.org/ftp/Haskell/partial-signatures.lhs and > even somewhat understood it; however, I tried to apply it to my config file > with an implicit parameter in the signature, and I couldn't get it to compile. > > Is there something inherently different about using this approach with > implicit parameters, or am I probably just doing something wrong? Example code (that is, the code you're trying to modify with an implicit parameter) would be useful. I'm not sure implicit parameters would work with that example anyway, as they aren't Haskell '98 and can't be emulated in Haskell '98 (at least, not that way). - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -BEGIN PGP SIGNATURE- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkx7zHAACgkQIn7hlCsL25UZCACg0OILDSnwXceO+gctbFwAcG5a zs4An0YZLmKDDt67xGzeWK2fNWLGZyiC =hwND -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Quick Question for QuickCheck2
Hello, perhaps I am just blind or is it a difficult issue: I would like to generate Char values in a given Range for QuickCheck2. There is this simple example from the haskell book: instance Arbitrary Char where arbitrary = elements (['A'..'Z'] ++ ['a' .. 'z'] ++ " ~...@#$%^&*()") This does not work in QuickCheck2 since the instance is already defined. How do I achieve this behaviour in QC2? Thanks for helping. Sebastian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Hackage on Linux
On 30 August 2010 11:26, Andrew Coppin wrote: > Stephen Tetley wrote: >> >> Windows has a standard place for header files >> >> \MinGW\include >> > > Isn't that "MinGW has a standard place for header files"? Strictly speaking its "Haskell-on-Windows has a standard place for header files". ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] getting started with HJscript?
Hi all, I'll probably have to be doing web stuff soon. And I think I would like to be using JavaScript far more than I have in the past. So I'm thinking about using Haskell (HJscript) to generate it for me. How does on go about learning how to use HJscript? Are there any examples / tutorials? Günther ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Partial Signatures with Implicit Parameters
I would like to specify that a function takes implicit parameters, without specifying its full return type. My main motivation for this is my xmonad config file and the attempt to remove the need for NoMonomorphismRestriction and some of the code smell associated with global variables that wafts in with implicit parameters. I have read this: http://okmij.org/ftp/Haskell/partial-signatures.lhs and even somewhat understood it; however, I tried to apply it to my config file with an implicit parameter in the signature, and I couldn't get it to compile. Is there something inherently different about using this approach with implicit parameters, or am I probably just doing something wrong? P.S. I decided to ask this here instead of in the xmonad mailing list because I feel like this is a question about haskell that was only slightly inspired by my use of xmonad. -- Alex R ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] open and closed
On 8/29/10 1:33 PM, Gábor Lehel wrote: Another thing I'm wondering about is that there's a fairly intuitive correspondence between functions at the value level vs. functions at the type level, and datatypes to classify the value level vs. datakinds to classify the type level, but what corresponds to type classes at the value level? Wouldn't you go the other way: kind classes? Type classes are predicates on types, and the application of a class to a type forms a proposition which represents the type of proofs that the proposition holds (i.e., the type of instance dictionaries). This can be easily extended upwards by having predicates on kinds yielding propositions that represent the kinds of (type-level) proofs. IIRC, this is the perspective that Omega takes. To extend it downward we'd have to ask what it would mean to have a predicate on values. The value-level propositions formed by applying those predicates couldn't have proofs (because there is no sub-value level), so it's not entirely clear what that would mean. If anything, the value-level correspondent of type classes are just uninterpreted predicates, i.e. data constructors. Whether this line of thinking is sensible or just a fallacious attempt to unify everything, I can't say off hand. I think it's better to think of contexts as the type of the invisible lambda for passing dictionaries, just as forall is the type of (the invisible) big-lambda, and -> is the type of lambda. Thus, the dictionaries are the concrete thing you want to generalize to higher levels; the classes will be at the next level up. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Contibution to Haskell world
crazy.fizruk: > Hi all, > > I am very interested in haskell and most of related things and as I know there > are a lot of things to do for haskell world. I have rather small, as I think, > expirience with haskell: I've worked with Language.C, alex, happy, parsec and > some other stuff that I haven't looked though attentively. Most of haskell > code > I've seen was highly readable and most of code I wrote was very easy to write. > So I liked to write in haskell and I want to make some contribution to its > world. As I am rather new to haskell world I ask you for a problem that can be > interesting for me and useful for haskell world. Today I am student at Moscow > State University and have at least 2 years for some kind of scientific work. > > P.S. Some interesting topics for me are transparent parallelization, parallel > and distibuted computing and computational models. However, many other topics > are also interesting for me =) > Thanks for helping! We have a list of problems on the proposals reddit: http://www.reddit.com/r/haskell_proposals/top/?t=year Perhaps something there is interesting to you? -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Contibution to Haskell world
Hi all, I am very interested in haskell and most of related things and as I know there are a lot of things to do for haskell world. I have rather small, as I think, expirience with haskell: I've worked with Language.C, alex, happy, parsec and some other stuff that I haven't looked though attentively. Most of haskell code I've seen was highly readable and most of code I wrote was very easy to write. So I liked to write in haskell and I want to make some contribution to its world. As I am rather new to haskell world I ask you for a problem that can be interesting for me and useful for haskell world. Today I am student at Moscow State University and have at least 2 years for some kind of scientific work. P.S. Some interesting topics for me are transparent parallelization, parallel and distibuted computing and computational models. However, many other topics are also interesting for me =) Thanks in advance, Nick ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Hackage on Linux
Stephen Tetley wrote: Windows has a standard place for header files \MinGW\include Isn't that "MinGW has a standard place for header files"? I'm guessing if you use DJGPP or MS VisualStudio or Borland C++, it's not going to look there (unless you tell it to). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Hackage on Linux
Regardless, you'd think Cabal could provide some way to make it "easy" to state where the files it needs actually are. Currently it does not. Well, it uses ghc-pkg to record where the various libraries, etc. are. Otherwise, it could be that none of the Cabal developers are really that familiar with the "best practices" of developing Windows software (and clobbering the registry whilst your at it). Note that Cabal is no better at tracking location of non-Haskell resources on Unix. (In fact, isn't that what started this topic?) Indeed. Windows lacks a standard place for developer files. By the way, is it possible to have a globally installed library in Windows (for C, etc.) that can be used no matter which IDE or editor you use? Or does each IDE manage all that on its own? DLLs can be put into C:\WINDOWS\SYSTEM32 or equivalent. More correctly: DLLs can be put *anywhere you like*, so long as they are registered in the Registry. And yes, it's quite possible to install libraries system-wide. Take DirectX, for example. Just about every Windows computer game installer begins by testing whether DirectX is installed, what version, and installing the version from the CD if newer (which it almost never is). [Actually, the cheap games just run the installer whatever; fortunately, the MS installer checks, sees it's already installed, and doesn't reinstall it again.] The DirectX DLLs aren't installed in a standard place; they're registered in the Registry, and that's how you find them. It's all about the Registry. LIB files are less standard and I'm under the impression that every IDE uses its own notion of where to put them (and may not use the registry in a non-opaque way). As best as I can tell, Windows has a standard way to locate *run-time* resources (e.g., DLLs), but not for *compile-time* resources (header files, LIB files, etc.) As I say, I think the intention is that once you've built the thing, it should run on any Windows box - which means it needs to be able to find stuff. But on the development box, you're expected to do the legwork to tell it where stuff is (or rather, tell the IDE which then manages stuff for you). Windows really is GUI-oriented rather than CLI-oriented. Perhaps you've noticed... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Support for lock-free/wait-free programming? / ANN: bits-atomic
On Sun, 29 Aug 2010 13:08:48 -0400, Gregory Collins wrote: > Gregory Collins writes: > ...sigh... The "programs link fine without it" part is a partial lie. > Anything that the C linker links (i.e. executables) works fine without > an explicit -lgcc_s, but ghci and compilations using template haskell > fail with an "unknown symbol `___bswapdi2'", or equivalent. > > Looking for a workaround now. After some more off-list discussion with Gregory (thanks for your help!) I split out the atomic operations to the bits-atomic package [1] which no longer depends on libgcc_s. GCC produces native code for atomic operations, so libgcc_s is not needed for these operations. Additionally, a test suite covering the most important operations is now included. I am still looking for a solution to drop the libgcc dependency for Data.Bits.Extras (which will remain in bits-extras) as well, but this is harder as the decision whether to use fall-back software implementations depends on the CPU capabilities. Cheers, Gabriel [1] http://hackage.haskell.org/package/bits-atomic-0.1.0 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly humorous: Headhunters toolbox (example for Germany)
On 27/08/10 23:45, sylvain wrote: Other sources show growing interest in Haskell (much to the dismay of our favorite motto). Would you accept to refer to these other sources? One interesting one is http://www.itjobswatch.co.uk/jobs/uk/haskell.do Paul. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ICFP Hotel Room
Hi Michael, I'm a graduate student (male) and am looking for a (male) roommate to split the cost of a hotel room at ICFP. [...] I currently have a reservation at the conference hotel If you don't find a roommate and can cancel your reservation you may consider staying somewhere else. For example, http://www.rodewayinnbaltimoremd.com/ is a 15 minutes walk from the conference hotel and less expensive. At last year's ICFP people were organising shared flats through the Haskell Wiki but I don't know whether this is repeated this year. Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher-order algorithms
One very nice example of a "higher-order" algorithm is the notion of region (i.e. Point -> Bool) defined in Hudak's paper, that is using functions as data structures... http://delivery.acm.org/10.1145/25/242477/a196-hudak.html?key1=242477&key2=4611513821&coll=GUIDE&dl=GUIDE&CFID=99830619&CFTOKEN=16057768 On Mon, Aug 23, 2010 at 6:03 AM, Eugene Kirpichov wrote: > Most of the well-known algorithms are first-order, in the sense that > their input and output are "plain" data. > Some are second-order in a trivial way, for example sorting, > hashtables or the map and fold functions: they are parameterized by a > function, but they don't really do anything interesting with it except > invoke it on pieces of other input data. > > Some are also second-order but somewhat more interesting: > * Fingertrees parameterized by monoids > * Splitting a fingertree on a monotonous predicate > * Prefix sum algorithms, again usually parameterized by a monoid or a > predicate etc. > > Finally, some are "truly" higher-order in the sense that is most > interesting to me: > * The Y combinator > * Difference lists > > Do there exist other nontrivial higher-order algorithms and datastructures? > Is the field of higher-order algorithms indeed as unexplored as it seems? > > I mean that not only higher-order facilities are used, but the essence > of the algorithm is some non-trivial higher-order manipulation. > > For example, parser combinators are not so interesting: they are a > bunch of relatively orthogonal (by their purpose) combinators, each of > which is by itself quite trivial, plus not-quite-higher-order > backtracking at the core. > > For example, for the Y combinator and difference lists are > interesting: the Y combinator builds a function from a function in a > highly non-trivial way; difference lists are a data structure built > entirely from functions and manipulated using higher-order mechanisms. > > > -- > Eugene Kirpichov > Senior Software Engineer, > Grid Dynamics http://www.griddynamics.com/ > ___ > 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
