[Haskell-cafe] Re: Cabal dependency hell
Edward Z. Yang wrote: Ivan Lazar Miljenovic's wrote: Edward Z. Yang writes: I doubt you'd get very much runtime with that. I'd suggest prompting the user to submit a failed build report if the build fails. Exactly like how Windows keeps prompting you to allow it to send an error report to Microsoft? I don't know about you, but I always found it irritating... I think the primary irritation is that Microsoft gets all of these error reports and they disappear into the great black VOID. Some public statistics might help alleviate the irritation. Perhaps exactly when the user is prompted? Would you like to send an anonymous report of this build failure to hackage.org? Users have been uploading 189 reports so far; yours would be the 190th report that ensures high quality Haskell packages! [y/n] Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal, GHC and Preprocessors
On Mon, 2010-04-12 at 06:51 +0100, Malcolm Wallace wrote: Even without that, it may be possible to get what you want, using -pgmPcpphs -optP-cpp -optP-ansi that is, to override ghc's addition of -traditional with -ansi. However I'm not sure exactly what order the preprocessor arguments will reach cpphs - in a choice between -traditional and -ansi, it is the last one on the cpphs commandline that will take effect. This worked in my .cabal file: cpp-options: --cpp -ansi ghc-options: -pgmPcpphs Thanks! -- Ashley Yakeley ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Cabal dependency hell
Heinrich Apfelmus apfel...@quantentunnel.de writes: Perhaps exactly when the user is prompted? Would you like to send an anonymous report of this build failure to hackage.org? Users have been uploading 189 reports so far; yours would be the 190th report that ensures high quality Haskell packages! [y/n] Which, in its own way, means that cabal-install is still phoning home; you then even need network access if you're building packages that you've already downloaded the sources for. -- 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
[Haskell-cafe] Re: [Haskell] Monads Terminology Question
Hi (Redirecting to cafe, for general chat.) On 12 Apr 2010, at 01:39, Mark Snyder wrote: Hello, I'm wondering what the correct terminology is for the extra functions that we define with monads. For instance, State has get and put, Reader has ask and local, etc. Is there a good name for these? Yes. Indeed, quite a lot of energy has been expended on the matter. It's worth checking out work by Plotkin and others on Algebraic Effects (often transmitted around Haskell-land by helpful citizens like Dan Piponi and Heinrich Apfelmus). This work distinguishes two kinds of extra function: operations (e.g. get, put, ask, throwError, etc) and control operators (local, catchError, etc). *Operations* have types like s1 - ... sn - M t where the s's and t are thought of as value types, and M is yer monad. You can think of M as describing an impure capability, permitting impure functions on values. You might even imagine specifying M's collection of operations by a signature, with this made up notation. sig M where f s1 ... sn :: t Note that I'm careful to mark with :: where the inputs stop and the outputs start, as higher-order functions make this ambiguous. For example sig State s where get :: s put s :: () sig Reader r where ask :: r sig Maybe where throw :: a Many popular monads can be characterized exactly by the signature of their operations and the equational theory those operations must obey (e.g. laws like put s get = f == put s f s). The point of these monads is to deliver the capability specified by the operations and equations. The similiarity between the signatures above and the typeclasses often declared to support monadic functionality is no coincidence. Note that every (set of) signature(s) induces a datatype of command-response trees whose nodes are labelled with a choice of operation and inputs, whose edges are labelled with outputs, and whose leaves carry return values. Such a tree represents a client strategy for interacting with a server which offers the capability, at each step selecting an operation to perform and explaining how to continue as a function of the value returned. The equational theory of the operations induces an equivalence on strategies. Command-response trees up to operational equivalence give the most general implementation of the specified monad: return makes leaves, = pastes trees together, and each operation creates a node. The monad comes from its operations! But what of local, catchError, and other such things? These are *control operators*, and they operate on computations, with types often involving resembling a - (b - M c) - M d Typically, the job of a control operator is to make local changes to the meaning of the operations in M's signature. A case in point is local, whose job is to change the meaning of ask. It's really shadowing one reader capability with another. Similarly, catchError can be thought of as offering a local exception. Old LISPheads (like me!) might think of operations as EXPRs and control operators as FEXPRs. Haskell does a neat job of hiding the distinction between the two, but it may be conceptually helpful to dig it out a bit. Control operators don't give rise to nodes in command-response trees; rather, they act as tree transformers, building new strategies from old. I could start a pantomime about why operations are heroes and control operators are villains, but I won't. But I will suggest that characterising monads in terms of the operations and/or control operators they support is a useful (and increasingly modular) way to manage effects in programming. After all, most end-user applications effectively equip a bunch of user-operations with a semantics in terms of system-operations. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal dependency hell
On Sun, 2010-04-11 at 18:43 +0200, Maciej Piechotka wrote: * Build reporting in the hackage server The idea here is that cabal sends back anonymous reports to the server to say if a package compiled or not, and against what versions of dependencies. This would make it clearer to maintainers if their dependency versions are correct. Additionally I think it would be useful for hackage to provide tweaked .cabal files for packages with updated constraints, even without new version uploads. We are proposing a GSoC project which would cover some of this. Hmm. I guess there are 2 problems: - Privacy problem. I don't want the software to call home with data without asking. Obviously it is important that the data be anonymous and that we do not send stuff without the user's knowledge. While there is not any directly identifying information in the existing anonymous build reports, one has to be very careful with how much access the server provides to the reports or it may become possible to infer identifying information. For example you might happen to know that I'm one of the few users on Sparc/Linux. Another possible attack is to try to discover timing of uploaded reports by the attacker inserting their own reports at regular intervals. If the server provided direct access to reports, in order of upload time, then this would give away timing of uploads. Similarly, if all reports were kept together then one could identify bunches of packages uploaded at the same time and infer they are from the same user. So yes, it needs careful thought. Perhaps we cannot give clients access to the raw reports at all. Perhaps it's enough to separate reports by package and to delay publishing new ones for a day or two, and to randomise the order when they are made available. - Spoofing problem. Someone can feed wrong data easily without chance of being discovered (for example to prove how grate 'haxor' he is). I don't think that's a major problem. One has to treat the data with that possibility in mind. There's also the option for authenticated non-anoymous reports with build logs. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal dependency hell
On Sun, 2010-04-11 at 14:28 -0700, Jason Dagit wrote: I've noticed another type of diamond dependency problem. Suppose I build and install Foo today and it depends on Bar 2.0.0. In a week, I install Bar 2.0.1. Next I installed Baz that also depends on Bar, and it gets Bar 2.0.1. When I install a package that depends on Foo, Baz, and possibly Bar, then cabal won't be able to figure out proper dependencies because Foo needs one version of Bar and Baz needs a different version. That's exactly the problem that cabal-install solves. It will rebuild one or the other of Foo and Baz so that the dependency on Bar is consistent. But if all these packages followed the PVP, then either version of Bar could have been used, if it was used consistently. Yes, but one would still need to be rebuilt. i'm not sure what is the best solution to this problem. Perhaps in this scenario, cabal should ask the user if it should rebuild Foo and/or Baz so they use the same Bar. I think this could lead to a lot of rebuilding, and that rebuilding gets tedious when you're doing it manually. So it happens automatically at the moment. It tries to minimise the amount of rebuilding. I occasionally hear complaints that it is rebuilding things when users did not expect it to. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal update problem
On Fri, 2010-02-19 at 12:21 +0100, Maciej Podgurski wrote: Hi, after updating to cabal-install-0.8.0/Cabal-1.8.0.2 with GHC 6.10.4, I always get an error when updating the package list: cabal update Downloading the latest package list from hackage.haskell.org cabal: Codec.Compression.Zlib: premature end of compressed stream Is there a way to fix this without rebuilding from the latest darcs repo? This is a public service announcement: Windows users should upgrade to cabal-install-0.8.2 Windows binary available here http://haskell.org/cabal/download.html I'll also be included in the upcoming release of the Haskell Platform. Sorry about the silly bug. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] dependent types
On Sun, Apr 11, 2010 at 10:54 PM, Jason Dagit da...@codersbase.com wrote:
Or, you could use witness types:
data Vehicle classification = Vehicle { ... }
mkCar :: Vehicle Car
mkTruck :: Vehicle Truck
Then you would export the smart constructors, (mkCar/mkTruck) without
exporting the Vehicle constructor.
moveVehicle :: Vehicle c - Simulation ()
carsOnly :: Vehicle Car - ...
In the witness type version you may find that defining Vehicle as a GADT is
even better:
data Vehicle classification where
mkCar :: ... - Vehicle Car
mkTruck :: ... - Vehicle Truck
A minor point of syntax: GADT constructors should begin with a capital letter.
A more important point: GADT constructors are useful for some things
but aren't appropriate for this case because they aren't smart -
they can't take an Int parameter and then make either a Car or a Truck
depending on its value. A smart constructor will need to account for
the possibility that the parameter isn't valid:
mkCar :: Integer - Maybe Vehicle
mkCar weight
| weight carWeight = Nothing
| otherwise = Car { weight = weight }
-- or
mkVehicle :: Integer - Vehicle
mkVehicle weight
| weight carWeight = Truck weight
| otherwise = Car weight
Even with GADTs, you can't pattern match on the constructors unless
you export them, in which case you have to allow for the possibility
that someone might construct an invalid value of the type, so you
might then also need smart field labels that retrieve values from
the Vehicle without allowing you to set them as well (as you would be
able to if you exported the field label itself).
Personally I think this approach is all rather OO. The way that seems
most natural to me is:
moveVehicleAcrossBridge :: Bridge - Vehicle - Maybe Move
moveVehicleAcrossBridge bridge { maxWeight = max } vehicle { weight = w }
| w max = Nothing
| otherwise = {- ... moving stuff ... -}
so you just test the properties directly as and when they are
interesting to you.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal dependency hell
Duncan Coutts duncan.cou...@googlemail.com writes: Here are a few things which I would like to see implemented that would help all this: * Build reporting in the hackage server The idea here is that cabal sends back anonymous reports to the server to say if a package compiled or not, and against what versions of dependencies. This would make it clearer to maintainers if their dependency versions are correct. It could also be checked before compilation. This would provide an incentive for the user to contribute, since she feels she's already getting something tangible back. And we've already asserted that the network is available. Perhaps it would also be possible to suggest library upgrades likely to remedy the problem in case of a build failure? -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Monads Terminology Question
Hi Conor William Harrison calls them 'non-proper morphisms' in his various papers modelling threads etc. using resumption monads. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] problem getting cabal-install to work on CentOS 5.2
Hi, I am trying to install cabal-install 0.8.2 with GHC 6.12.1 on a CentOS 5.2 system and am running up against a 'ExitFailure 127' error. I can download the package and run 'cabal install' inside the package directory and all will be fine, but if I let cabal download and install the package cabal runs into problems as soon as it tries to configure. For example, if I try 'cabal install permutation --verbose=3' it finishes like this: link: done *** Deleting temp files: Deleting: /tmp/ghc1324_0/ghc1324_0.lpp *** Deleting temp dirs: Deleting: /tmp/ghc1324_0 /tmp/permutation-0.4.132758/permutation-0.4.1/dist/setup/setup configure --verbose=3 --ghc --prefix=/home/chris/.cabal --user --constraint=base ==3.0.3.2 --constraint=ghc-prim ==0.2.0.0 cabal: Error: some packages failed to install: permutation-0.4.1 failed during the configure step. The exception was: ExitFailure 127 I have tried the same exercise with GHC 6.10.4 with cabal-install 0.8.0 the same results. I have downloaded the Cabal sources to try and add some instrumentation to find out what is going wrong I have yet to succeed. Does anybody have any suggestions? Is there an easier way of getting cabal-install working on CentOS? Any help much appreciated! Chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Monads Terminology Question
Hi Stephen On 12 Apr 2010, at 13:00, Stephen Tetley wrote: Hi Conor William Harrison calls them 'non-proper morphisms' in his various papers modelling threads etc. using resumption monads. I like Bill's work on resumptions, but I'm not entirely convinced by this phrase, which strikes me (possibly incorrectly) as arising from a local need for a term for 'the extra stuff', rather than a deeper analysis of the structure of effectful computation. Why it is a matter of propriety is beyond me. I'm realistic about the nature of naming as a social process, so I won't spend many tears on it. Truth to tell, I'm proposing to use the *vocabulary* of the algebraic effects people, mostly because I'd like to promote their *ideas* (which fit quite well with Bill's, I think). All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Cabal dependency hell
Ivan Lazar Miljenovic wrote: Heinrich Apfelmus writes: Perhaps exactly when the user is prompted? Would you like to send an anonymous report of this build failure to hackage.org? Users have been uploading 189 reports so far; yours would be the 190th report that ensures high quality Haskell packages! [y/n] Which, in its own way, means that cabal-install is still phoning home; you then even need network access if you're building packages that you've already downloaded the sources for. Good point. How about using a cached number from the last cabal install , then: Would you like to send an anonymous report of this build failure to hackage.org? Users have been uploading more than 188 reports so far to help ensure high quality Haskell packages! [y/n] It's just to instill a sense of activity and purpose. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal dependency hell
On Mon, Apr 12, 2010 at 4:00 AM, Duncan Coutts duncan.cou...@googlemail.com wrote: On Sun, 2010-04-11 at 14:28 -0700, Jason Dagit wrote: I've noticed another type of diamond dependency problem. Suppose I build and install Foo today and it depends on Bar 2.0.0. In a week, I install Bar 2.0.1. Next I installed Baz that also depends on Bar, and it gets Bar 2.0.1. When I install a package that depends on Foo, Baz, and possibly Bar, then cabal won't be able to figure out proper dependencies because Foo needs one version of Bar and Baz needs a different version. That's exactly the problem that cabal-install solves. It will rebuild one or the other of Foo and Baz so that the dependency on Bar is consistent. Weird. This has not been my experience. Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] Monads Terminology Question
Hi Conor Chuan-kai Lin uses 'effect basis' in the ICFP paper on the Unimo monads, otherwise I've seen 'operations' used. I'm on the fence for 'effect basis' vs. 'non-proper morphisms', but biased against 'operations' (as its not sufficiently characteristic). Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] dependent types
On Mon, Apr 12, 2010 at 4:32 AM, Ben Millwood hask...@benmachine.co.ukwrote:
Personally I think this approach is all rather OO. The way that seems
most natural to me is:
moveVehicleAcrossBridge :: Bridge - Vehicle - Maybe Move
moveVehicleAcrossBridge bridge { maxWeight = max } vehicle { weight = w }
| w max = Nothing
| otherwise = {- ... moving stuff ... -}
so you just test the properties directly as and when they are
interesting to you.
The problem with this is that it doesn't address the question the OP had.
The OP's question was how to enforce things at the type level, but this,
while being a valid approach, allows heavy vehicles to attempt the bridge
crossing. I agree it's a nice way of encoding it, but if type level
enforcement is called for then I don't see how it applies.
Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] dependent types
On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit da...@codersbase.com wrote:
On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
fr...@geoinfo.tuwien.ac.at wrote:
in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with size
less than a constant. big_boat is a vessel with a larger size. for
example, many legal classifications are expressed in this form (e.g. car
vs. truck)
depending on the type, operations are applicable or not (e.g. road with
restriction 'no trucks').
In the witness type version you may find that defining Vehicle as a GADT is
even better:
data Vehicle classification where
mkCar :: ... - Vehicle Car
mkTruck :: ... - Vehicle Truck
This is nice because it's direct and when you pattern match on the
constructor you recover the type of classification. For example, I believe
this would type check:
foo :: Vehicle c - c
foo (mkCar ...) = Car
foo (mkTruck ...) = Truck
You can combine GADTs with a mirror type for views of that data.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
module GADTSmart (VehicleView(..), Vehicle, Car, Truck,
mkCar, mkTruck, view) where
data Car
data Truck
data Vehicle t where
VCar :: Int - Vehicle Car
VTruck :: Int - Vehicle Truck
data VehicleView t where
VVCar :: Int - VehicleView Car
VVTruck :: Int - VehicleView Truck
view :: Vehicle t - VehicleView t
view (VCar wt) = VVCar wt
view (VTruck wt) = VVTruck wt
mkCar :: Int - Maybe (Vehicle Car)
mkCar wt | wt 2000 = Just (VCar wt)
| otherwise = Nothing
mkTruck :: Int - Maybe (Vehicle Truck)
mkTruck wt | wt = 2000 = Just (VTruck wt)
| otherwise = Nothing
-- Client code that doesn't have access to the VCar or VTruck
-- constructors.
moveAcrossBridge :: Vehicle Car - IO ()
moveAcrossBridge c = case view c of
VVCar wt - putStrLn $ Car (++show wt++) on bridge
Now you can type your functions with the Vehicle GADT, but only
introduce values of that type using smart constructors. You could use
the VVCar or VVTruck data constructors to create invalid values, but
they won't work your functions.
Anthony
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] mingw32_HOST_OS and friends
Where can I find a list of such symbols and what they mean? Google finds lots of uses but no definitions, and I'd like to avoid guessing. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANN: vcd-0.0.0
I uploaded a small library [1] for generating VCD files [2], which can be viewed with waveform tools like GTKWave [3]. Though VCD is commonly associated with Verilog simulation, at Eaton we use it to visualize vehicle data in realtime: data is pulled off the CAN bus, formated to VCD, then piped into GTKWave. Most operations are in the IO monad, but if there's a better way to do it, I'm open to suggestions. I hope to add a simple VCD parser to the library soon; again suggestions welcome. -Tom [1] http://hackage.haskell.org/package/vcd [2] http://en.wikipedia.org/wiki/Value_change_dump [3] http://en.wikipedia.org/wiki/GTKWave ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: dependent types
On Mon, 2010-04-12 at 12:44 -0400, Anthony Cowley wrote:
On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit da...@codersbase.com wrote:
On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
fr...@geoinfo.tuwien.ac.at wrote:
in modeling real application we have often the case that the type of
some object depends on a value. e.g. small_boat is a vessel with size
less than a constant. big_boat is a vessel with a larger size. for
example, many legal classifications are expressed in this form (e.g. car
vs. truck)
depending on the type, operations are applicable or not (e.g. road with
restriction 'no trucks').
In the witness type version you may find that defining Vehicle as a GADT is
even better:
data Vehicle classification where
mkCar :: ... - Vehicle Car
mkTruck :: ... - Vehicle Truck
This is nice because it's direct and when you pattern match on the
constructor you recover the type of classification. For example, I believe
this would type check:
foo :: Vehicle c - c
foo (mkCar ...) = Car
foo (mkTruck ...) = Truck
You can combine GADTs with a mirror type for views of that data.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
module GADTSmart (VehicleView(..), Vehicle, Car, Truck,
mkCar, mkTruck, view) where
data Car
data Truck
data Vehicle t where
VCar :: Int - Vehicle Car
VTruck :: Int - Vehicle Truck
data VehicleView t where
VVCar :: Int - VehicleView Car
VVTruck :: Int - VehicleView Truck
view :: Vehicle t - VehicleView t
view (VCar wt) = VVCar wt
view (VTruck wt) = VVTruck wt
mkCar :: Int - Maybe (Vehicle Car)
mkCar wt | wt 2000 = Just (VCar wt)
| otherwise = Nothing
mkTruck :: Int - Maybe (Vehicle Truck)
mkTruck wt | wt = 2000 = Just (VTruck wt)
| otherwise = Nothing
-- Client code that doesn't have access to the VCar or VTruck
-- constructors.
moveAcrossBridge :: Vehicle Car - IO ()
moveAcrossBridge c = case view c of
VVCar wt - putStrLn $ Car (++show wt++) on bridge
Now you can type your functions with the Vehicle GADT, but only
introduce values of that type using smart constructors. You could use
the VVCar or VVTruck data constructors to create invalid values, but
they won't work your functions.
Anthony
http://www.willamette.edu/~fruehr/haskell/evolution.html
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
data Zero = Zero
data Succ a = Succ a
class Peano a where
fromPeano :: a - Integer
instance Peano Zero where
fromPeano _ = 0
instance forall a. Peano a = Peano (Succ a) where
fromPeano _ = 1 + fromPeano (undefined :: a)
class (Peano a, Peano b) = LT a b
instance Peano b = LT Zero (Succ b)
instance LT a b = LT a (Succ b)
instance LT a b = LT (Succ a) (Succ b)
class (Peano a, Peano b) = EQ a b
instance EQ Zero Zero
instance EQ a b = EQ (Succ a) (Succ b)
class (Peano a, Peano b) = GT a b
instance LT a b = GT b a
class (Peano a, Peano b) = LEQ a b
instance EQ a b = LEQ a b
instance LEQ a b = LEQ a (Succ b)
class (Peano a, Peano b) = GEQ a b
instance EQ a b = GEQ a b
instance GEQ a b = GEQ (Succ a) b
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
data Car = Car
data Truck = Truck
data Vehicle s v where
VCar :: LT size Five = Vehicle size Car
VTruck :: GEQ size Five = Vehicle size Truck
Regards
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] Re: [Haskell] Monads Terminology Question
Sorry to interject a noob comment, and maybe I am not understanding the question but why not just call MonadState etc. Monad subclasses? get and put would then be Monad subclass functions. -deech On 4/12/10, Stephen Tetley stephen.tet...@gmail.com wrote: Hi Conor Chuan-kai Lin uses 'effect basis' in the ICFP paper on the Unimo monads, otherwise I've seen 'operations' used. I'm on the fence for 'effect basis' vs. 'non-proper morphisms', but biased against 'operations' (as its not sufficiently characteristic). Best wishes Stephen ___ 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] ANNOUNCE: darcs 2.4.1
Hi all, The darcs team would like to announce the immediate availability of darcs 2.4.1. This release fixes a number of issues that were found in darcs 2.4. The most important of these issues were that darcs did not work on Windows shares, and that darcs would not work if it was built with a wrong version of the mmap package. The easiest way to install darcs is using the Haskell Platform [1]. If you have installed the Haskell Platform or cabal-install, you can install this release by doing: $ cabal update $ cabal install --reinstall darcs Alternatively, you can download the tarball from http://darcs.net/releases/darcs-2.4.1.tar.gz and build it by hand as explained in the README file. What's New -- * Important changes in Darcs 2.4.1 * darcs works again on Windows network shares * missing documentation and test files have been added to the tarball * darcs will no longer give errors about a nonexistent file when compiled with the wrong mmap * moving files between directories can no longer break the directory index * darcs handles the case that someone uses 'remove -r' on an untracked directory * darcs ignores symlinks again, like all pre-2.4 releases * Bugs Fixed in Darcs 2.4.1 * 1645: ignore symlinks * 1750: uncover help text for 'darcs show pristine' * 1753: restrict mmap to version used by hashed-storage * 1754: fix issue458.sh on systems with xattrs * 1756: moving files between directories breaks index * 1757: add test files to distribution tarball * 1765: refuse to remove non-tracked directories recursively * 1767: send CRC erros to standard error Reporting bugs -- If you have an issue with darcs 2.4.1, you can report it via the web on http://bugs.darcs.net/ . You can also report bugs by email to b...@darcs.net. Kind Regards, the darcs release manager, Reinier Lamers [1]: You can download the Haskell platform from http://hackage.haskell.org/platform/ 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
[Haskell-cafe] Re: [Haskell] Monads Terminology Question
From: Conor McBride co...@strictlypositive.org To: Mark Snyder muddsny...@yahoo.com; haskell Cafe haskell-cafe@haskell.org Sent: Mon, April 12, 2010 5:34:05 AM Subject: Re: [Haskell] Monads Terminology Question Hi (Redirecting to cafe, for general chat.) On 12 Apr 2010, at 01:39, Mark Snyder wrote: Hello, I'm wondering what the correct terminology is for the extra functions that we define with monads. For instance, State has get and put, Reader has ask and local, etc. Is there a good name for these? Yes. Indeed, quite a lot of energy has been expended on the matter. It's worth checking out work by Plotkin and others on Algebraic Effects (often transmitted around Haskell-land by helpful citizens like Dan Piponi and Heinrich Apfelmus). Thanks! I wasn't aware of that work. It certainly does split things up nicely, I hadn't really thought of looking at them as two distinct groups of functionality. It also clears things up in my mind to look at them as the maximum-arity functions and seeing whether any arguments are computations, or whether the function just constructs a computation. This work distinguishes two kinds of extra function: operations (e.g. get, put, ask, throwError, etc) and control operators (local, catchError, etc). *Operations* have types like s1 - ... sn - M t where the s's and t are thought of as value types, and M is yer monad. You can think of M as describing an impure capability, permitting impure functions on values. You might even imagine specifying M's collection of operations by a signature, with this made up notation. sig M where f s1 ... sn :: t Note that I'm careful to mark with :: where the inputs stop and the outputs start, as higher-order functions make this ambiguous. For example sig State s where get :: s put s :: () sig Reader r where ask :: r sig Maybe where throw :: a Many popular monads can be characterized exactly by the signature of their operations and the equational theory those operations must obey (e.g. laws like put s get = f == put s f s). The point of these monads is to deliver the capability specified by the operations and equations. The similiarity between the signatures above and the typeclasses often declared to support monadic functionality is no coincidence. Note that every (set of) signature(s) induces a datatype of command-response trees whose nodes are labelled with a choice of operation and inputs, whose edges are labelled with outputs, and whose leaves carry return values. Such a tree represents a client strategy for interacting with a server which offers the capability, at each step selecting an operation to perform and explaining how to continue as a function of the value returned. The equational theory of the operations induces an equivalence on strategies. Command-response trees up to operational equivalence give the most general implementation of the specified monad: return makes leaves, = pastes trees together, and each operation creates a node. The monad comes from its operations! But what of local, catchError, and other such things? These are *control operators*, and they operate on computations, with types often involving resembling a - (b - M c) - M d Typically, the job of a control operator is to make local changes to the meaning of the operations in M's signature. A case in point is local, whose job is to change the meaning of ask. It's really shadowing one reader capability with another. Similarly, catchError can be thought of as offering a local exception. Old LISPheads (like me!) might think of operations as EXPRs and control operators as FEXPRs. Haskell does a neat job of hiding the distinction between the two, but it may be conceptually helpful to dig it out a bit. Control operators don't give rise to nodes in command-response trees; rather, they act as tree transformers, building new strategies from old. I could start a pantomime about why operations are heroes and control operators are villains, but I won't. But I will suggest that characterising monads in terms of the operations and/or control operators they support is a useful (and increasingly modular) way to manage effects in programming. After all, most end-user applications effectively equip a bunch of user-operations with a semantics in terms of system-operations. All the best Conor So in this line of thought, where we have the operations and the control operators, I guess my original question wasn't aware of the distinction, and was looking for a name for all of them combined. In Haskell (specifically in the mtl), we see them lumped together into the typeclass. If we are talking about an implementation, is it good practice to try and use the most theoretically correct language, even if an implementation diverges somewhat while getting things done? I.e., should they be referred to as the operations and control operators, or more simply as the type-class-provided functions? I like the
Re: [Haskell-cafe] Re: [Haskell] Monads Terminology Question
On 12 April 2010 20:43, aditya siram aditya.si...@gmail.com wrote: [SNIP] ... why not just call MonadState etc. Monad subclasses? get and put would then be Monad subclass functions. Hi At a pinch, that would tie them into their (Haskell) implementation technique. Picking an example I'm somewhat familiar with, Andrzej Filinski defined equivalents in SML using structures - where I think he simply called them 'operations'. Best wishes Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
