Re: [Haskell-cafe] Zipper and Comonad
Hi Mathijs On 22 May 2012, at 07:42, Mathijs Kwik wrote: Hi all, After using zippers for a while, I wanted to dig a bit deeper into them. I found there is some relation between Zipper and Comonad, but this confuses me somewhat. After reading a bit more about Comonads [1] and [2], I think I understand them somewhat, and I see how they too are useful for navigating a data structures and giving functions the ability to look around. What confuses me though, is the relation between these 2. This source [3] mentions all zippers can be made instances of Comonad, and demonstrates how to do this for simple, 1-dimensional (list) zippers. But a comment on [4] says a Zipper by itself is already an application of Comonad. I want to find out which is the case. Looking at the types does not yield me a solution yet. [..] Once upon a time, I wrote this message: http://www.haskell.org//pipermail/libraries/2010-July/013843.html which may serve as grist to your mill. The key points (1) Inductive datatypes can usually be seen as instances of data Mu f = In (f (Mu f)) where f is a Functor explaining the structure of one node, with the parameter of f standing for the node's children. See how Mu f instantiates f's parameter with Mu f, meaning that the children are recursive subobjects? (2) The derivative f' of such an f characterizes f-structures with one element missing, so a one-hole context in a Mu f is given by the type [f' (Mu f)], being a series of nodes, each of which has one child missing, but whose other children are still intact. The whole zipper is given by ([f' (Mu f)], Mu f) (3) The construction Focusf x = (f' x, x), representing an f-node with one child held separately, is always comonadic. The counit gives the separated child, discarding the context. The cojoin decorates each element with its own context, showing the decompositions you could get by moving the cursor. Sorry to be so brief and example-free -- terrible hurry Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Data Kinds and superfluous (in my opinion) constraints contexts
Hi Simon On 10 May 2012, at 13:19, Simon Peyton-Jones wrote: I'm glad you've been trying out kinds. However, I don't understand the feature you want here. You say: fromIntgr :: Integer - BV (size :: D) fromIntgr int = BV mkD int -- doesn't work, but desired. fromIntgr :: MkD size = Integer - BV (size :: D) fromIntgr int = BV mkD int -- does work, but is not that useful. The implementation MUST pass a value parameter for (MkD size =) to fromIntgr. Your point is presumably that since every inhabitant of kind D is an instance of MkD, the (MkD size =) doesn't actually constrain the type at all. It really works for every instantiation of 'size'. So maybe your feature is Please omit class constraints where I can see that every suitably-kinded argument is an instance of the class. So we're dealing with the difference between pi and forall. It's clear that promotion alone doesn't really deliver the pi behaviour. That still currently requires the singleton construction, which SHE automates, at least in simple cases. (Shameless plug: see my answer on StackOverflow this morning http://stackoverflow.com/questions/10529360/recursively-defined-instances-and-constraints) I suppose that might be conceivable, but it'd make the language more complicated, and the implementation, and I don't see why the second version is not that useful. Start a feature-request ticket if you like, though. There's a bunch of competing notions to negotiate. Once we have a promotable type, e.g., data Nat = Zero | Succ Nat we get a singleton family data Natty :: Nat - * where Zeroy :: Natty Zero Succy :: Natty n - Natty (Suc n) (In fact, SHE has one data family for the singleton construction, and generates suitable data instance declarations, here mapping Nat to Natty.) As Serguey makes clear, we should also get a class like class HasNatty :: Nat - Constraint where natty :: Natty n instance HasNatty Zero where natty = Zeroy instance HasNatty n = HasNatty (Succ n) where natty = Succy natty Again, SHE automates this construction. The constraint HasNatty n is written (with distinctive ugliness) {:n :: Nat:}, as is the witness, desugaring to the equivalent of (natty :: Natty n). We can then play spot-the-difference between (1) forall (n :: Nat). (2) forall (n :: Nat). Natty n - (3) forall (n :: Nat). HasNatty n = (1) is genuinely different; (2) and (3) are equivalent but have different pragmatics. (1) does not involve any runtime data, and has stronger free theorems; (2) involved runtime data passed explicitly and readily pattern-matched (for which SHE also has a notational convenience); (3) involves runtime data passed implicitly. (2) is somehow the explicit pi of dependent type theory (and it's how SHE translates pi); (3) is somehow the implicit pi; (1) is somehow the irrelevant pi (which is an abuse of the letter pi, as the notion is an intersection rather than a product). I'd like to be able to (and SHE lets me) write (2) as pi (n :: Nat). I'd like to be able to (and SHE doesn't let me) write (3) as (n :: Nat) = I see one main dilemma and then finer variations of style. The dilemma is EITHER make forall act like pi for promoted datatypes, so that runtime witnesses are always present OR distinguish pi from forall, and be explicit when runtime witnesses are present Traditional type theory does the former but is beginning to flirt with the latter, for reasons (better parametricity, more erasure) that have value in theory and practice. I regard the latter as a better fit with Haskell in any case. However, it would be good to automate the singleton construction and sugar over the problem, and even better to avoid the singleton construction just using Nat data in place of Natty data. Other dilemmas. If we have have distinct pi and forall, which do we get when we leave out quantifiers? I'd suggest forall, as somehow the better fit with silence and the more usual in Haskell, but it's moot. When we write instance Applicative (Vector n)-- (X) we currently mean, morally, instance forall (n :: Nat). Applicative (Vector n) -- (X) which we can't define, because pure needs the length at runtime. But perhaps we should write instance pi (n :: Nat). Applicative (Vector n) or (if this syntax is unambiguous) instance (n :: Nat) = Applicative (Vector n) both of which would bring n into scope as a runtime witness susceptible to case analysis. There is certainly something to be done (and SHE already does some of it, within the limitations of a preprocessor). I'd be happy to help kick ideas around, if that's useful. All the best Conor Simon | -Original Message- | From: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe- | boun...@haskell.org] On Behalf Of Serguey Zefirov | Sent: 06 May 2012 17:49 | To: haskell | Subject: [Haskell-cafe] Data Kinds and superfluous (in my opinion) |
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 23 Dec 2011, at 16:16, MigMit wrote: On 23 Dec 2011, at 02:11, Conor McBride wrote: So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)? The plan is to make a clearer distinction between being and doing by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [list of effects]value type is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. Oh, so it's not an arbitrary monad, but a single one. That's a bit disappointing. The list of effects is arbitrary, and localizable, by means of defining handlers. So it's not a single monad. It's probably still disappointing. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 22 Dec 2011, at 17:49, Bardur Arantsson wrote: Alexander Solla wrote: I happen to only write Haskell programs that terminate. It is not that hard. We must merely restrict ourselves to the total fragment of the language, and there are straight-forward methods to do so. Do (web/XML-RPC/whatever) server type programs terminate? No, but total and terminating are not the same. Those *co*programs will, if they're any good, be total by virtue of their productivity rather than their termination. What's slightly controversial is the claim that we must merely restrict ourselves to the total fragment of the language. It would be more controversial to claim that some new Haskell-like language should restrict us to total programs. I'd be glad if pure meant total, but partiality were an effect supported by the run-time system. Then we could choose to restrict ourselves, but we wouldn't be restricted by the language. This is not the first time the issue has surfaced, nor will it be the last. It's customary at this point to object that one wouldn't want to program with the monadic notation, just for the effect of partiality. I'd counter that I don't want to program with the monadic notation, for any effects: I'd like to program with an applicative notion, but in monadic types. That's what I'd do different, and for me, the subject is not a hypothetical question. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 22 Dec 2011, at 21:29, MigMit wrote: Отправлено с iPad 22.12.2011, в 23:56, Conor McBride co...@strictlypositive.org написал(а): I'd be glad if pure meant total, but partiality were an effect supported by the run-time system. Then we could choose to restrict ourselves, but we wouldn't be restricted by the language. I second that. Having a special partiality monad would be nice. However, I'm not certain as to how it would interact with recursion — if f is a total function, fix f could be (and almost certainly would be) a possibly undiefined value. So, fix should have type (a - a) - Partial a; that's OK, but implicit uses of fix (I mean let statements) would be quite different. Indeed they would, at least to the extent of making clear in the type on what basis recursive calls should be checked. I'd like to program with an applicative notion, but in monadic types. That's what I'd do different, and for me, the subject is not a hypothetical question. So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)? The plan is to make a clearer distinction between being and doing by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [list of effects]value type is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. But it is always possible to make a value type from a computation type by suspending it (with braces), so that {[list of effects]value type} is a value type for suspended computations, which *are* things which one could potentially *do* at another time. But we can manipulate suspended computations purely. Haskell doesn't draw a clear line in types between the effect part and the value part, or support easy fluidity of shifting roles between the two. Rather we have two modes: (1) the implicit partiality mode, where the value part is the whole of the type and the notation is applicative; (2) the explicit side-effect mode, where the type is an effect operator applied to the value type and the notation is imperative. It's an awkward split, and it makes it tricky to make clean local renegotiations of effectful capabilities by hiding or handling them. Also, I don't see why partiality deserves an applicative notation where other, perhaps more benign effects (like *handled* exceptions) are forced into an imperative (or clunky Applicative) mode. Maybe this strays too far to classify as Haskell-like, but it's an attempt to re-rationalise techniques that emerged from Haskell programming. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Alternative versus Monoid
On 21 Dec 2011, at 14:07, Erik Hesselink hessel...@gmail.com wrote: On Wed, Dec 21, 2011 at 14:10, Bas van Dijk v.dijk@gmail.com wrote: The semantics of Maybe are clear: it's failure-and-prioritized-choice. Are you sure? Yes. There are (at least) four Monoid instances for Maybe [1]. With a direct instance for Maybe and its Dual you have only covered two. Types don't just give data a representation: types evoke structure. The data stored by Maybe can be made into a monoid in several ways, but the failure-management role of Maybe makes just one of them appropriate. Cheers Conor Erik [1] https://byorgey.wordpress.com/2011/04/18/monoids-for-maybe/ ___ Libraries mailing list librar...@haskell.org http://www.haskell.org/mailman/listinfo/libraries ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Alternative versus Monoid
On 15 Dec 2011, at 15:19, Brent Yorgey wrote: On Thu, Dec 15, 2011 at 06:49:13PM +1000, Gregory Crosswhite wrote: So at the end of the day... what is the point of even making Maybe and [] instances of Alternative? The Alternative and Monoid instances for [] are equivalent. However, the Alternative and Monoid instances for Maybe are not. To wit: (Just (Sum 4)) | (Just (Sum 3)) Just (Sum {getSum = 4}) (Just (Sum 4)) `mappend` (Just (Sum 3)) Just (Sum {getSum = 7}) The current monoid instance for Maybe is, in my view, unfortunate. Types are about semantic purpose, not just data representation. Many purposes can be represented in the same way. We should identify the purpose of a type (or type constructor), then define instances consistent with that purpose. And better, we acquire by instance inference compound instances consistent with that purpose! (A similar view is often articulated well by Conal Elliott. But perhaps it's just a Con thing.) The purpose of Maybe, it seems to me, is to model failure and prioritized choice, after the manner of exceptions. It's clear what the failure-and-prioritized-choice monoid is. It so happens that the same data representation can be used to make a semigroup into a monoid by attaching an identity element. That's a different semantic purpose, which deserves a different type. This really bites. I really like being able to write things like newtype P a x = P ([a] - Maybe (x, [a])) deriving Monoid and then make MonadPlus/Alternative instances just by copying the monoid that results, but it doesn't work! It's unfortunate that we don't have local quantification in constraints, so we can't write (forall x. Monoid (f x)), hence the need for constructor classes doing basically the same job, with, of necessity, newly renamed members. I think it compounds the problem to choose inconsistent behaviour between the constructor class and the underlying type class. Maybe I'm an extremist, but I'd prefer it if every Alternative instance was constructed by duplicating a polymorphic Monoid instance. Meanwhile, as for the issue which kicked this off, I do think it's good to document and enforce meaningful (i.e. total on total input) usages of operations by types where practical. At present, refining one type class into several to account for subtle issues (like whether some/many actually work) is expensive, even if it's desirable. I'd once again plug default superclass instances and Control.Newtype, then suggest that the library might benefit from a little pruning. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] PhD Position available at Strathclyde
[My colleague, Patricia Johann, advertises the following...] PhD Position in Category Theory and Functional Programming Department of Computer and Information Sciences University of Strathclyde, Scotland Applications are invited for one PhD position within the Mathematically Structured Programming group at the University of Strathclyde. The group comprises Prof. Neil Ghani, Dr. Patricia Johann, Dr. Conor McBride, Dr. Peter Hancock, Dr. Robert Atkey, and six PhD students. The PhD project centres around applications of categorical methods to functional programming languages. The project is under the direction of Patricia Johann. The successful applicant will have either a first-class degree or an MSc in Mathematics or Computing Science or a related subject with a strong Mathematics or Computing Science component. Ideally, they will also have a strong, documented interest in doing research. Strong mathematical background and problem-solving skills are essential; good programming skills are a plus. Prior knowledge of category theory and/ or functional programming is an advantage, but is not required. The PhD position is for 3 years; it starts in January 2012. The position is a fully-funded post for a UK or EU student, and includes both coverage of fees and an EPSRC-level stipend for each of the three years. More information about the department is available at http://www.strath.ac.uk/cis The University of Strathclyde (http://www.strath.ac.uk) is located in the heart of Glasgow, which Lonely Planet Travel Guides hail as one of Britain's largest, liveliest and most interesting cities (seehttp://www.lonelyplanet.com/worldguide/scotland/glasgow/) . Southern Scotland provides a particularly stimulating environment for researchers in theoretical computer science, with active groups in this area at Heriot-Watt University, the University of Edinburgh, the University of Glasgow, the University of St. Andrews, and the University of Strathclyde. Requests for further information and other informal enquiries can be sent to: Patricia Johann patricia at cis.strath.ac.uk Those interested in the position are asked to send e-mail to the address given above in the next short while. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Another(!) PhD Position at Strathclyde
Hot on the heels of Patricia Johann's advertisement, here's another PhD Position in the Mathematically Structured Programming Group, Deparment of Computer and Information Sciences at the University of Strathclyde to be supervised by Dr. Conor McBride and Prof. Neil Ghani on something related to Designing Precision with Dependent Types. We invite applications for one PhD position within the Mathematically Structured Programming group at the University of Strathclyde. The group comprises Prof. Neil Ghani, Dr. Patricia Johann, Dr. Conor McBride, Dr. Peter Hancock, Dr. Robert Atkey, and five PhD students. The PhD project involves THEORETICAL and PRACTICAL issues in FUNCTIONAL PROGRAMMING with DEPENDENT TYPES. Dependent type systems allow us to construct precise variations on general-purpose datatypes which address the specific needs of particular programming problems, thus opening a new precision axis in the design space of programs and data. We seek equipment to help programmers explore this axis, determining what is needed to shift the level of precision at which existing functions operate and which properties are guaranteed in return. The project thus represents an opportunity to study mathematical abstractions with a concrete engineering motivation. The PhD position is for 3 years, starting in October 2011. The position is a fully-funded post for a UK or EU student, and includes coverage both of fees and an EPSRC-level stipend for each of the three years. More information about the department is available at http://www.strath.ac.uk/cis The University of Strathclyde (http://www.strath.ac.uk) is slap bang in the middle of Glasgow, a thronging metropolis of wit and daring. Scotland is a hive of activity in Computer Science: we have active collaborations with researchers at Edinburgh, Heriot-Watt, Glasgow and St. Andrews. This is the time and the place to make an impact. Requests for further information and other informal enquiries can be sent to: Conor McBride conor at cis.strath.ac.uk Please get in touch as soon as you can. We hope to appoint in early May. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
On 17 Mar 2011, at 18:35, wren ng thornton wrote: Another question on particulars. When dealing with natural numbers, we run into the problem of defining subtraction. There are a few reasonable definitions: No there aren't. Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is SHE (the Strathclyde Haskell Enhancement) portable?
On 23 Jan 2011, at 11:27, Maciej Piechotka wrote: It may be strange question but: - Is SHE portable (assuming that the compiler have the extensions)? I have no idea. - If yes why there is only information how to use it with GHC? I'm lucky I even know how to get it to work with GHC. It'd be a bonus if it turned out to be portable. If anyone figures out how to bolt it on the front of other compilers, I'd be happy to relay (with attribution) the relevant instructions on the SHE website. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is SHE (the Strathclyde Haskell Enhancement) portable?
On 23 Jan 2011, at 18:19, Maciej Piechotka wrote: On Sun, 2011-01-23 at 18:42 +0100, Lennart Augustsson wrote: It probably is portable, but I'd think only GHC has all the necessary extensions. I imagine some parts (idiom brackets) works with minimal amount of extentions - maybe it would be benefitial to have instructions to run SHE with other compilers? Yes, idiom brackets, default superclass instances, that sort of stuff is all good clean H98 fun. I'm open to code and/or doc patches, but I'm unlikely to have time to take the initiative. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proposal: Applicative = Monad: Call for consensus
Hi Tyson (So OT, I'm switching to cafe.) On 19 Jan 2011, at 18:24, Tyson Whitehead wrote: On January 17, 2011 16:20:22 Conor McBride wrote: Ahem : ) The unfortunate pain you pay for this additional power is manually having to specify the application ($ and *) and merging (join). If the compiler could figure this all out for you based on the underlying types, wow! To achieve such a thing, one would need to ensure a slightly more deliberate separation of value and computation in the presentation of types. In Haskell, we use, e.g., [Int], for * pure computations of lists of integers * nondeterministic computations of integers [..] I'm pretty sure I know what pure computations of lists of integers is, but I'm not so sure about nondeterministic computations of integers. If it is not too much of an effort, could you clarify with a quick example? Viewing [] as a monad, you can view [1,2] as a nondeterministic integer with possible values 1 and 2. Lifting operations to this monad gives you all possible combinations computation, so, as SHE would have it, (| [1,2] + [3,4] |) = pure (+) * [1,2] * [3,4] = [4,5,5,6] It's not hard to come up with examples where lifted and unlifted both make sense. With a bit of help from Twitter, we have (courtesy of Andy Gimblett) ([under,over] ++ [state,wear]) = [under,over,state,wear] but (|[under,over] ++ [state,wear]|) = [understate,underwear,overstate,overwear] and (courtesy of Dan Piponi) ([plan,tan] ++ [gent,king]) = [plan,tan,gent,king] but (|[plan,tan] ++ [gent,king]|) = [plangent,planking,tangent,tanking] In each case, the former has (++) acting on lists of strings as pure values, while the latter has (++) acting on strings as values given in []-computations. The type [String] determines a domain, it does not decompose uniquely to a notion of computation and a notion of value. We currently resolve this ambiguity by using one syntax for pure computations with [String] values and a different syntax for [] computations with String values. Just as we use newtypes to put a different spin on types which are denotationally the same, it might be worth considering a clearer (but renegotiable) separation of the computation and value aspects of types, in order to allow a syntax in which functions are typed as if they act on *values*, but lifted to whatever notion of computation is ambient. After types for representation, let us have types for explanation. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generalizing catMaybes
On 8 Jan 2011, at 11:14, Henning Thielemann wrote: For me, the solutions of Dave Menendez make most sense: Generalize Maybe to Foldable and List to MonadPlus. What has it to do with monads? There's no bind in sight. Alternative is certainly a more general alternative, but then I would say that, wouldn't I? Even that seems a tad too much. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generalizing catMaybes
On 8 Jan 2011, at 15:27, Henning Thielemann wrote: On Sat, 8 Jan 2011, Conor McBride wrote: On 8 Jan 2011, at 11:14, Henning Thielemann wrote: For me, the solutions of Dave Menendez make most sense: Generalize Maybe to Foldable and List to MonadPlus. What has it to do with monads? There's no bind in sight. I see a '=' in front of each of his expressions. That'll teach me to wake up first. Sorry. If you have some m (f x), and you make an (m x) from each inner x, then you do need something joiny. Of course, there is an alternative generalisation. [] and Maybe are both Foldable, hence so is their composition. There's got to be a thing of type collapse :: (Foldable f, Alternative a) = f x - a x which would do the job. Of course, anything which is both foldable and alternative certainly has a function with the type of join. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's the motivation for η rules?
Hi Thus invoked... On 28 Dec 2010, at 23:29, Luke Palmer wrote: Eta conversion corresponds to extensionality; i.e. there is nothing more to a function than what it does to its argument. Suppose f x = g x for all x. Then using eta conversion: f = (\x. f x) = (\x. g x) = g Without eta this is not possible to prove. It would be possible for two functions to be distinct (well, not provably so) even if they do the same thing to every argument -- say if they had different performance characteristics. Eta is a controversial rule of lambda calculus -- sometimes it is omitted, for example, Coq does not use it. It tends to make things more difficult for the compiler -- I think Conor McBride is the local expert on that subject. ...I suppose I might say something. The motivation for various conversion rules depends quite a lot on one's circumstances. If the primary concern is run-time computation, then beta-rules (elimination construct consumes constructor) and definitional expansion (sometimes delta), if you have definition, should do all the work you need. I'm just wondering how to describe such a need. How about this property (reminiscent of some results by Herman Geuvers). Let = be the conversion relation, with whatever rules you've chucked in, and let -- be beta+delta reduction, with --* its reflexive-transitive closure. Suppose some closed term inhabiting a datatype is convertible with a constructor form t = C s1 .. sn then we should hope that t --* C r1 .. rn with ri = si, for i in 1..n That is: you shouldn't need to do anything clever (computing backwards, eta-conversion) to get a head-normal form from a term which is kind enough to have one. If this property holds, then the compiler need only deliver the beta-delta behaviour of your code. Hurrah! So why would we ever want eta-rules? Adding eta to an *evaluator* is tedious, expensive, and usually not needed in order to deliver values. However, we might want to reason about programs, perhaps for purposes of optimization. Dependent type theories have programs in types, and so require some notion of when it is safe to consider open terms equal in order to say when types match: it's interesting to see how far one can chuck eta into equality without losing decidability of conversion, messing up the Geuvers property, or breaking type-preservation. It's a minefield, so tread carefully. There are all sorts of bad interactions, e.g. with subtyping (if - subtyping is too weak, (\x - f x) can have more types than f), with strictness (if p = (fst p, snd p), then (case p of (x, y) - True) = True, which breaks the Geuvers property on open terms), with reduction (there is no good way to orientate the unit type eta-rule, u = (), in a system of untyped reduction rules). But the news is not all bad. It is possible to add some eta-rules without breaking the Geuvers property (for functions it's ok; for pairs and unit it's ok if you make their patterns irrefutable). You can then decide the beta-eta theory by postprocessing beta-normal forms with type-directed eta-expansion (or some equivalent type-directed trick). Epigram 2 has eta for functions, pairs, and logical propositions (seen as types with proofs as their indistinguishable inhabitants). I've spent a lot of time banging my head off these issues: my head has a lot of dents, but so have the issues. So, indeed, eta-rules make conversion more extensional, which is unimportant for closed computation, but useful for reasoning and for comparing open terms. It's a fascinating, maddening game trying to add extensionality to conversion while keeping it decidable and ensuring that open computation is not too strict to deliver values. Hoping this is useful, suspecting that it's TMI Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] Functor = Applicative = Monad
On 15 Dec 2010, at 17:48, Brent Yorgey wrote: On Wed, Dec 15, 2010 at 06:25:30PM +0100, Maciej Piechotka wrote: On Wed, 2010-12-15 at 13:51 +0200, John Smith wrote: On 15/12/2010 11:39, Lennart Augustsson wrote: Any refutable pattern match in do would force MonadFail (or MonadPlus if you prefer). So [..] As far as type inference and desugaring goes, it seems very little would have to be changed in an implementation. Is there a need for a MonadFail, as distinct from mzero? fail always seems to be defined as error in ordinary monads, and as mzero in MonadPlus (or left at the default error). Not all types can implement mplus to begin with even if they can have 'zero' type. For example technically Maybe breaks the laws while still having useful fail: [..] But that depends on what laws you choose for MonadPlus. See http://www.haskell.org/haskellwiki/MonadPlus . What has any of this to do with monads? Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] Functor = Applicative = Monad
[switching to cafe] On 14 Dec 2010, at 08:59, Sittampalam, Ganesh wrote: John Smith wrote: I would like to formally propose that Monad become a subclass of Applicative, with a call for consensus by 1 February. I would prefer that we have some proposal like class aliases implemented before we start fundamental restructuring of basic type classes. This would help to limit the disruption these changes cause, which will be substantial. I'm inclined to agree. What's even more galling than not having Functor and Applicative instances for Monads is having to write them! At the very least, can we open this particular vessel of vermicular splendidity and verify that the inmates are still grinning with persistence? If I recall, the class alias proposal was rather more ambitious than necessary to solve this problem (though that is no crime), but still a little wrinkled in the corners. Looking at the relevant webpages, I see the proposal has lots of attractive motivational examples, but less by way of definition. But perhaps, somewhere, it has been defined enough for a prototype? It's surely worth looking at some way to define default instances for superclasses, provided they can be overridden or switched off. Where did this train of though leave the rails, again? Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] libffi mystery
Hi Thanks for the help! I've made some progress, but I'm not there yet. On 28 Oct 2010, at 20:08, Ketil Malde wrote: Sittampalam, Ganesh ganesh.sittampa...@credit-suisse.com writes: Have you tried passing -optl-static to ghc (which causes -static to be passed to ld)? This was new to me. I gave it a whirl. I got lots of linker errors about missing pthread this, missing pthread that, so... It used to be: -optl-static -optl-pthread ...seemed like a good plan. I got lots of scary warnings like (.text+0x51d8): warning: Using 'setprotoent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/haskell-packages/ghc6/lib/network-2.2.1.7/ghc-6.12.1/ libHSnetwork-2.2.1.7.a(BSD.o): In function `suy9_info': (.text+0x12f6): warning: Using 'endprotoent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/haskell-packages/ghc6/lib/network-2.2.1.7/ghc-6.12.1/ libHSnetwork-2.2.1.7.a(BSD.o): In function `svAk_info': but an executable emerges. If I run the executable from the prompt, it dumps some html, but it still 500s on the web server. So there are at least options and ways to control what's going on. I haven't figured out how to achieve the 6.8.2-alike linking, but oughtn't it to be possible? Many thanks Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] cabal mystery (#562?)
Hi I've just installed cabal-install (just as a user: I am nowhere near root) on our unix server at work. That went fine. Clearly, the sensible thing to do next is get hold of an up-to-date package list. So, I tried co...@cafe:~$ cabal update Downloading the latest package list from hackage.haskell.org cabal: Codec.Compression.Zlib: premature end of compressed stream Here's the verbose version. co...@cafe:~$ cabal -v3 update Downloading the latest package list from hackage.haskell.org Sending: GET http://hackage.haskell.org/packages/archive/00-index.tar.gz HTTP/1.1 User-Agent: cabal-install/0.8.2 Host: hackage.haskell.org proxy uri host: www-cache.strath.ac.uk, port: :8080 Creating new connection to www-cache.strath.ac.uk:8080 Received: HTTP/1.0 200 OK Date: Thu, 28 Oct 2010 12:59:17 GMT Server: Apache/2.2.9 (Debian) mod_python/3.3.1 Python/2.5.2 Last-Modified: Thu, 28 Oct 2010 12:38:17 GMT ETag: 1888003-20bb4e-493ac9dbe6040 Accept-Ranges: bytes Content-Length: 2145102 Content-Type: application/x-tar Content-Encoding: x-gzip X-Cache: MISS from rouble-1.cc.strath.ac.uk X-Cache-Lookup: MISS from rouble-1.cc.strath.ac.uk:8080 Via: 1.1 rouble-1.cc.strath.ac.uk:8080 (squid/2.7.STABLE7) Connection: close Downloaded to /home/s3/conor/.cabal/packages/hackage.haskell.org/00-index.tar.gz cabal: Codec.Compression.Zlib: premature end of compressed stream So I poked about a bit, and I see it's a known issue. As a user, I'm wondering what to do. Just now, wget http://hackage.haskell.org/packages/archive/00-index.tar.gz is chugging away quite nicely. Anyhow, is there (a) something I can do to avoid this problem? I couldn't quite grasp what to do from the TRAC (b) some way to persuade cabal to use the file I'm currently downloading? Any tips to keep the gremlins at bay gratefully appreciated. Thanks Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] libffi mystery
Hi again This is what happens when you write actual for-users for-running programs, I guess. It's been a while... I've been writing some software with Network.CGI etc, which we run on the deparmental web server for my students to use. But we just had a bit of an upgrade on the system, and now (once cabal was properly installed) everything compiles again but nothing works. The reason appears to be that the executables now depend on a dynamic library libffi.so.5 which is not (and I am told cannot become) available on our web server. The current workaround is to compile with 6.8.2, which is survivable and will hopefully get me through the semester, but not ideal. Is there some way I can get some more static linking to happen? I did poke about online a bit and found some remarks to the effect that GHC got so much more portable after switching to the dynamic libffi. That sounds great, but tough luck for me. So, being both powerless and clueless, I can only ask: how hosed am I? I'd be grateful for any glimmers of light. Thanks Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CFP MSCS Issue: Dependently Typed Programming
(s:S)-(p:P s)*(s:S)-(p:P s)*(s:S)-(p:P s)*(s:S)-(p:P s)*(s:S)- (p:P s)* OPEN CALL FOR PAPERS for a Special Issue of MATHEMATICAL STRUCTURES in COMPUTER SCIENCE in association with the workshop DEPENDENTLY TYPED PROGRAMMING 2010 editors: Thorsten Altenkirch (Nottingham), Conor McBride (Strathclyde) 2011 timeline: submission Jan 31; notification May 31; final version June 30 (s:S)-(p:P s)*(s:S)-(p:P s)*(s:S)-(p:P s)*(s:S)-(p:P s)*(s:S)- (p:P s)* Thorsten Altenkirch and Conor McBride are delighted to invite contributions to a Special Issue of the journal Mathematical Structures in Computer Science (Cambridge University Press), in association with the Workshop on Dependently Typed Programming, which we organised on 9 and 10 July 2010 in Edinburgh, as part of FLoC, associated with LiCS. The workshop had a packed programme of exciting developments, reflecting the strength of work on this topic at this time. More recent workshops and conferences have exhibited a significant contribution from researchers in this area. We are grateful to Editor-in-Chief Giuseppe Longo and to Editor Eugenio Moggi for the opportunity to reflect these welcome developments in the pages of MSCS, and we encourage researchers to consider submitting a paper. submission deadline: January 31 2011 notification: May 31 2011 final versions due: June 30 2011 We invite full journal articles concerning Dependently Typed Programming or related topics, from authors at work in this area. Submissions are particularly welcome from but not limited to contributors to the workshop, and the same journal-standard peer review process will apply in any case. Please feel free to address any enquiries about scope and suitability to the guest editors, Thorsten Altenkirch (University of Nottingham) and Conor McBride (University of Strathclyde). Submissions should usually not exceed 35 pages. Authors should adhere to the guidelines issued by Cambridge University Press for MSCS contributors: http://assets.cambridge.org/MSC/MSC_ifc.pdf. These include directions to the relevant LaTeX resources. We very much look forward to hearing from you. Thorsten and Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
On 28 May 2010, at 08:47, Lennart Augustsson wrote: Yes, of course you have to trust Djinn to believe its proof. That's no different from having to trust me if I had done the proof by hand. Our you would have to trust yourself if you did the proof. BTW, Djinn does not do an exhaustive search, since there are infinitely many proofs. (Even if you just consider cut free proofs there's usually infinitely many.) Just to flesh out the thought, let me sketch completeness (the result is due to Roy Dyckhoff). Fortunately, an exhaustive search is not necessary for completeness in this logic. Let's say that a cycle in a proof is where some atomic proposition P is derived by a proof tree which includes internal derivations of P ... - P .. - P Of course, you can simplify such a proof by replacing the larger P-proof with the smaller. If a proposition has a proof, then it has a cycle-free proof. An exhaustive search of the cycle-free proofs is thus complete. But can we implement such a search? Given that an assumption can prove at most one atomic formula (an assumption which does not hold in *predicate* logic), you can be sure that any path in a proof tree which uses the same assumption twice creates a cycle. Correspondingly, you can be sure that in each branch of a proof, you can discard the assumptions you've already used. That's enough of a resource bound to ensure that an exhaustive search of the cycle-free proofs will terminate. (You can acquire new assumptions when you backchain on a higher-order assumptions, but the new assumptions are two orders lower than the assumption disposed of, so you can readily construct an order-based lexicographic termination scheme (shameless plug for my PAR2010 talk).) So, there's some reason to believe that there is a complete algorithm, which might even be the one Lennart implemented in Djinn. All the best Conor On Fri, May 28, 2010 at 8:14 AM, wren ng thornton w...@freegeek.org wrote: Lennart Augustsson wrote: So what would you consider a proof that there are no total Haskell functions of that type? Or, using Curry-Howard, a proof that the corresponding logical formula is unprovable in intuitionistic logic? It depends on what kind of proof I'm looking for. If I'm looking for an informal proof to convince myself, then I'd probably trust Djinn. If I'm trying to convince others, am deeply skeptical, or want to understand the reasoning behind the result, then I'd be looking for a more rigorous proof. In general, that rigorous proof would require metatheory (as you say)--- either my own, or understanding the metatheory behind some tool I'm using to develop the proof. For example, I'd only trust Djinn for a rigorous proof after fully understanding the algorithms it's using and the metatheory used to prove its correctness (and a code inspection, if I didn't trust the developers). If Djinn correctly implements the decision procedure that have been proven to be total (using meta theory), then I would regard Djinn saying no as a proof that there is no function of that type. So would I. However, that's adding prerequisites for trusting Djinn--- which was my original point: that Djinn says there isn't one is not sufficient justification for some folks, they'd also want justification for why we should believe Djinn actually does exhaust every possibility. -- Live well, ~wren ___ 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
[Haskell-cafe] DTP10 Call for Participation
Remember, Haskell is the world's most popular dependently typed functional programming language... (s:S)*(p:P s)-(s:S)*(p:P s)-(s:S)*(p:P s)-(s:S)*(p:P s)-(s:S)*(p:P s)- DTP 2010 --- Call for Participation EARLY REGISTRATION ENDS 17 MAY 2010 Workshop on DEPENDENTLY TYPED PROGRAMMING Edinburgh, Scotland, 910 July 2010 (a FLoC workshop, affiliated with LICS) http://sneezy.cs.nott.ac.uk/darcs/dtp10/ (s:S)*(p:P s)-(s:S)*(p:P s)-(s:S)*(p:P s)-(s:S)*(p:P s)-(s:S)*(p:P s)- Roll up! Roll up! Register early, register often! http://www.floc-conference.org/registration.html Attendance at DTP10 can be yours at a BARGAIN price if you register BEFORE 17 MAY 2010. The preliminary programme for DTP10 is here: http://sneezy.cs.nott.ac.uk/darcs/dtp10/programme.html Invited Talks: Ana Bove, Chalmers University, 10 Years of Partiality and General Recursion Matthieu Sozeau, Harvard University, Elaborations in Type Theory Contributed Talks: Edwin Brady, Practical, efficient programming with dependent types James Caldwell, Extracting Monadic Programs form Proofs, (joint work with Josef Pohl) Adam Chlipala, Generating Pieces of Web Applications with Type-Level Programming Nils Anders Danielsson, TBA Larry Diehl, Unit integration test composition via lemmas Makoto Hamana, Another Initial Algebra Semantics of Inductive Families for Programming Hugo Herbelin, A sequent calculus presentation of the Calculus of Inductive Constructions (joint work with Jeffrey Sarnat, Vincent Siles) Karim Kariso, Integrating Agda and Automated Theorem Proving Techniques (joint work with Anton Setzer) Dan Licata, Security-Typed Programming within Dependently Typed Programming (joint work with Jamie Morgenstern) Ulf Norell, TBA Carsten Schuermann, The HOL-Nuprl connection in Delphin, (joint work with Adam Poswolsky) Anton Setzer, Coalgebras in dependent type theory Antonis Stampoulis, VeriML: Type-safe computation of logical terms inside a language with effects Tarmo Uustalu, TBA Sean Wilson, Supporting Dependently Typed Functional Programming with Proof Automation and Testing If, by some chance, you are interested in talking at DTP10, please do get in touch. Space in the programme is now very tight, but we remain open to proposals. See you in Edinburgh in July! Thorsten and Conor ___ Agda mailing list a...@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] DTP10 Call for Participation
On 6 May 2010, at 16:04, Colin Paul Adams wrote: Conor == Conor McBride co...@strictlypositive.org writes: Conor Remember, Haskell is the world's most popular dependently Conor typed functional programming language... Could you justify that claim please? Is that a feature request or a sceptical objection? If the former, I'm on the case already. If the latter... avec plaisir. Which part of it do you dispute? That Haskell is a dependently typed functional programming language? Justification: cabal install she I know. It's not Haskell in the sense that the language compiled by GHC is not Haskell. The genie is far enough out of the bottle. Or is it my claim that Haskell is more popular than the other dependently typed programming languages? Judging by community traffic, Haskell is more popular than Coq. By construction, Haskell is at least as popular as Agda. I could name a few others (e.g., ATS, Idris), but they're clearly not touching Haskell for presence. Now, of course, the dependently typed functionality available in Haskell is a bit rudimentary compared to functional languages defined with dependent types in mind. I certainly don't think Haskell is popular for being dependently typed, or that dependently typed programmers favour Haskell as weapon-of-choice (actually, for language *implementation*, many of us do), but I was careful not to claim either of those things. Haskell has data-indexed types, via a suitable encoding, which SHE automates, and even some dependency on run-time data, via a singleton type encoding (the ugliness of which SHE does her best to tidy away). Everything you need to start experimenting with indexing your data and control structures is in the box already. Indexed versions of Functor and Monad are already beginning to emerge and prove useful. Indexed Monads are just what you get when you yank Hoare Logic through the Curry-Howard correspondence from proof to programming. Key question: how should the library equip us to exploit these notions effectively? So I will finish with some bold speculation, as it's election day and I've constructed enough content-free sloganeering already. If you want to use a bit of dependent typing pervasively in a real world application, linking with a wealth of libraries, Haskell's likely to be your best bet. For now. For a while yet, actually. Interesting times Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell and the Software design process
On 3 May 2010, at 02:18, Edgar Z. Alvarenga wrote: On Sun, 02/May/2010 at 13:10 -0700, Don Stewart wrote: * Avoid partial functions Why? Tell you tomorrow. Conor ___ 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] 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
Re: [Haskell-cafe] Re: ANN: data-category, restricted categories
Getting back to the question, whatever happened to empty case expressions? We should not need bottom to write total functions from empty types. Correspondingly, we should have that the map from an empty type to another given type is unique extensionally, although it may have many implementations. Wouldn't that make any empty type initial? Of course, one does need one's isogoggles on to see the uniqueness of the initial object. An empty type is remarkably useful, e.g. as the type of free variables in closed terms, or as the value component of the monadic type of a server process. If we need bottom to achieve vacuous satisfaction, something is a touch amiss. Cheers Conor On 30 Mar 2010, at 22:02, Edward Kmett ekm...@gmail.com wrote: The uniqueness of the definition of Nothing only holds up to isomorphism. This holds for many unique types, products, sums, etc. are all subject to this multiplicity of definition when looked at through the concrete-minded eye of the computer scientist. The mathematician on the other hand can put on his fuzzy goggles and just say that they are all the same up to isomorphism. =) -Edward Kmett On Tue, Mar 30, 2010 at 3:45 PM, wagne...@seas.upenn.edu wrote: Quoting Ashley Yakeley ash...@semantic.org: data Nothing I avoid explicit undefined in my programs, and also hopefully non- termination. Then the bottomless interpretation becomes useful, for instance, to consider Nothing as an initial object of Hask particularly when using GADTs. Forgive me if this is stupid--I'm something of a category theory newbie--but I don't see that Hask necessarily has an initial object in the bottomless interpretation. Suppose I write data Nothing2 Then if I understand this correctly, for Nothing to be an initial object, there would have to be a function f :: Nothing - Nothing2, which seems hard without bottom. This is a difference between Hask and Set, I guess: we can't write down the empty function. (I suppose unsafeCoerce might have that type, but surely if you're throwing out undefined you're throwing out the more frightening things, too...) ~d ___ 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] Linguistic hair-splitting
Hi On 27 Jan 2010, at 20:14, Luke Palmer lrpal...@gmail.com wrote: On Wed, Jan 27, 2010 at 11:39 AM, Jochem Berndsen joc...@functor.nl wrote: Now, here's the question: Is is correct to say that [3, 5, 8] is a monad? In what sense would this be a monad? I don't quite get your question. I think the question is this: if m is a monad, then what do you call a thing of type m Int, or m Whatever. It has been known to call such things 'computations', as opposed to 'values', and even to separate the categories of types and expressions which deliver the two. I think that's a useful separation: I wish return (embedding values in computations) were silent, and thunk (embedding computations in values) made more noise. Cheers Conor Luke ___ 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] Linguistic hair-splitting
On 27 Jan 2010, at 22:02, Daniel Fischer daniel.is.fisc...@web.de wrote: Am Mittwoch 27 Januar 2010 22:50:35 schrieb Conor McBride: It has been known to call such things 'computations', as opposed to 'values', and even to separate the categories of types and expressions which deliver the two. As usual, that only works part of the time. [1,4,15,3,7] is not a computation, it's a list of numbers. A plain and simple everyday value. Yes, the separation is not clear in Haskell. (I consider this unfortunate.) I was thinking of Paul Levy's call-by-push-value calculus, where the distinction is clear, but perhaps not as fluid as one might like. Int list values and nondeterministic int computations are conceptually different, even if they have isomorphic representations. Identifying their types has its downsides. Cheers Conor ___ 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] (liftM join .) . mapM
Hi Tony On 29 Dec 2009, at 12:10, Tony Morris wrote: Can (liftM join .) . mapM be improved? (Monad m) = (a - m [b]) - [a] - m [b] You can (a) generalize m from Monad to Applicative (b) generalize [b] to any Monoid (c) generalize [a] to f a for any Foldable f and write ala AppLift foldMap if you happen to have some of my usual kit. See below. Cheers Conor Here's the machinery. class Newtype n where type Unwrap n wrap :: Unwrap n - n unwrap :: n - Unwrap n ala :: Newtype v' = (t - t') - ((s - t') - u - v') - (s - t) - u - Unwrap v' ala p h f u = unwrap (h (p . f) u) Here's a rather useful newtype, capturing applicative lifting of monoids. newtype AppLift a x = AppLift (a x) instance (Applicative a, Monoid x) = Monoid (AppLift a x) where mempty = AppLift (pure mempty) mappend (AppLift ax) (AppLift ay) = AppLift (mappend $ ax * ay) instance Newtype (AppLift a x) where type Unwrap (AppLift a x) = a x wrap = AppLift unwrap (AppLift ax) = ax ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: (liftM join .) . mapM
Hi Maciej On 29 Dec 2009, at 20:52, Maciej Piechotka wrote: On Tue, 2009-12-29 at 18:20 +, Conor McBride wrote: ala AppLift foldMap What is benefit of it over: concatMapA f = foldr (liftA2 mappend . f) (pure mempty) Given that applicative functors take monoids to monoids, it's nice to exploit that property by name, rather than reconstructing it by engineered coincidence. I reuse the library pattern once (AppLift) that you reinvent in two places (liftA2 mappend) (pure mempty). (Ironically, foldr is defined in terms of foldMap by code that amounts to, modulo a flip, ala Endo foldMap appealing to the monoid of endomorphisms.) The result is an operation which (a) points out the essential mechanism, foldMap; (b) points out the structures on which it works, lifted monoids; (c) is short enough not to bother naming. More structure, less code, Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Re: (liftM join .) . mapM
Hi Maciej On 30 Dec 2009, at 00:07, Maciej Piechotka wrote: On Tue, 2009-12-29 at 23:00 +, Conor McBride wrote: Hi Maciej On 29 Dec 2009, at 20:52, Maciej Piechotka wrote: On Tue, 2009-12-29 at 18:20 +, Conor McBride wrote: ala AppLift foldMap What is benefit of it over: concatMapA f = foldr (liftA2 mappend . f) (pure mempty) Given that applicative functors take monoids to monoids, it's nice to exploit that property by name, rather than reconstructing it by engineered coincidence. I wouldn't state it as 'coincidence'. I don't need to create explicit map where implicit (liftA2 mappend and pure mempty) is sufficient. The coincidence I mean is *between* liftA2 mappend and pure mempty: those are the pieces of a lifted monoid, without the observation that that's what's going on. In this case I have one line when you have many (however it might be other case with more complicated examples - but I don't quite see how)[1]. It depends how you count. I have three symbols. The rest may not be in the standard library, but it's in my library. I certainlt wouldn't propose setting up that machinery just for that one problem. But if you google, you'll find I've suggested it several times, for a number of different problems. Also I'm not quite sure if ala is something general and therefore should be exposed instead of just putting it. But I may be wrong I've been programming with ala for some years now. I find it really useful. Zooming out a bit, I think there's a very healthy trend to introduce type distinctions at a finer level than is necessary for purposes of data representation, just to put a particular structural spin on things. The payback from that is writing less code, provided your library is set up to exploit richer type information. [1] http://www.willamette.edu/~fruehr/haskell/evolution.html ;) Quite so. I like evolving. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GHC 6.12 on OS X 10.5
Hi I thought I'd record my upgrade exerience (so far) in case anyone else finds it useful, and (more selfishly) in case anyone has some helpful advice. Summary of situation * I got 6.12 working. * It took a lot of fumbling around. * The eventual fix (renaming /opt/local/lib/libiconv.dylib) was a bit dodgy, but is holding for now. Long rambling narrative follows. Various features of GHC 6.12 made it very tempting to go for an earlier upgrade than I normally would. (SHE really needs GADT-style data families; everything I do needs deriving Traversable (deriving HalfZip would be nice too!).) Already there was a handy installer for Intel+Leopard macs (is anybody on the PPC+Leopard case? if not, I will be soon...). I thought go for it. Installation, no problem. Compiling something: whoops, no mtl. OK, cabal install mtl: whoops, no acceptable cabal. Fair dos, if I'd read the warnings I'd have known that my cabal-install would be useless and tried to build the new one. QUESTION: Is the sensible upgrade path to build cabal-install 0.8 with your old GHC, before installing 6.12? Does this even work? At one point, I tried this and had some peculiar issues involving zlib... Anyhow, I've got 6.12 and I need cabal-install 0.8. Can I find it? Tricky, and http://haskell.org/cabal/ didn't help much. I'm very tolerant of busy people not quite getting round to it, and I can use google, so I find the darcs version and get cracking. This happens: - bash-3.2$ ./bootstrap.sh Checking installed packages for ghc-6.12.1... parsec-2.1.0.1 will be downloaded and installed. network-2.2.1.5 will be downloaded and installed. Cabal is already installed and the version is ok. mtl-1.1.0.2 will be downloaded and installed. HTTP-4000.0.8 will be downloaded and installed. zlib-0.5.2.0 will be downloaded and installed. Downloading parsec-2.1.0.1... % Total% Received % Xferd Average Speed TimeTime Time Current Dload Upload Total Spent Left Speed 100 15430 100 154300 0 12743 0 0:00:01 0:00:01 --:--:-- 19312 [1 of 1] Compiling Main ( Setup.hs, Setup.o ) Linking Setup ... Undefined symbols: _iconv_close, referenced from: _hs_iconv_close in libHSbase-4.2.0.0.a(iconv.o) _iconv, referenced from: _hs_iconv in libHSbase-4.2.0.0.a(iconv.o) _iconv_open, referenced from: _hs_iconv_open in libHSbase-4.2.0.0.a(iconv.o) ld: symbol(s) not found collect2: ld returned 1 exit status Error during cabal-install bootstrap: Compiling the Setup script failed - At lthis point, I suspected a linker/dylib problem, but foolishly, I wanted the problem to be pretty much anything else, so I spent far too long looking the wrong way. I thought that if I could just get cabal-install working somehow, I'd be ok. I tried installing parsec with runhaskell Setup.hs {configure,build,install} but each of these commands appeared content to do precisely nothing: I found this perplexing. I tried reverting to 6.10.4 and compiling cabal-install. This made more progress, but died with some sort of zlib version snafu. (I'm sorry, I should have recorded the details but didn't.) The zlib-0.5.2.0 package did install successfully, but somehow the build for cabal-install itself went awry with an even though this is the right version I can't find X sort of a problem. I uninstalled 6.10.4, deleted my .cabal directory, nuked a few other relics showing up from what's probably a dumb choice of PATH setting. I had another go at 6.12, and this time I tried compiling a wee program of my own with no exciting package dependencies. Should have done that straight away, of course. Same iconv problem. This left no alternative. I found I had a /usr/lib/libiconv.dylib etc and an /opt/local/lib/libiconv.dylib etc, so I renamed the latter to opt/local/lib/moolibiconv.dylib, and suddenly, GHC became capable of linking stuff. The darcs version of cabal-install then built just fine; SHE rebuilt ok; Epigram needed a few extra LANGUAGE pragmas, but no trouble. I'm almost back where I was. I worry about this. (1) What have I broken by shifting the opt/local/lib copy of libiconv? (2) Why did that break things anyway? (3) How come I ended up with a broken library setup? (4) What else is broken? (What's worse than finding a maggot in your apple? Finding half a maggot in your apple.) I'm not at all a mac expert (I use a mac because I'm too stupid to maintain a linux installation -- the Nottingham grad students (all grown up now) told me they were fed up fixing my computer back in 04.) This dylib nonsense seems quite common. Is it MacPorts messing things up? Is there a more principled fix than the brutal thing I did? I wonder if it might be possible to build some sort of diagnostic tool to check paths
Re: [Haskell-cafe] Restrictions on associated types for classes
Hi all On 17 Dec 2009, at 14:22, Tom Schrijvers wrote: class MyClass k where type AssociatedType k :: * Is there a way of requiring AssociatedType be of class Eq, say? Have you tried: {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} class Eq (AssociatedType k) = MyClass k where type AssociatedType k :: * I just got very excited about this. I'm supposed to be setting a test, but this is far more interesting. I tried this {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls, TypeOperators #-} module DDD where class (Diff (D f)) = Diff f where type D f plug :: D f x - x - f x newtype K a x = K a deriving Show data Void magic :: Void - a magic x = x `seq` error haha instance Diff (K a) where type D (K a) = K Void plug (K c) x = magic c newtype I x = I x deriving Show instance Diff I where type D I = K () plug (K ()) x = I x data (f :+: g) x = L (f x) | R (g x) deriving Show instance (Diff f, Diff g) = Diff (f :+: g) where type D (f :+: g) = D f :+: D g plug (L f') x = L (plug f' x) plug (R g') x = R (plug g' x) data (f :*: g) x = f x : g x deriving Show instance (Diff f, Diff g) = Diff (f :*: g) where type D (f :*: g) = (D f :*: g) :+: (f :*: D g) plug (L (f' : g)) x = plug f' x : g plug (R (f : g')) x = f : plug g' x But I got this message [1 of 1] Compiling DDD ( DDD.lhs, interpreted ) DDD.lhs:5:2: Cycle in class declarations (via superclasses): DDD.lhs:(5,2)-(7,28): class (Diff (D f)) = Diff f where { type family D f; } Failed, modules loaded: none. and now I have to go back to setting my class test. Sorry for spam Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Restrictions on associated types for classes
On 17 Dec 2009, at 15:31, Simon Peyton-Jones wrote: Hmm. If you have class (Diff (D f)) = Diff f where then if I have f :: Diff f = ... f = e then the constraints available for discharging constraints arising from e are Diff f Diff (D f) Diff (D (D f)) Diff (D (D (D f))) ... That's a lot of constraints. But isn't it a bit like having an instance Diff f = Diff (D f) ? Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Implicit newtype unwrapping
Hi Martijn On 3 Dec 2009, at 00:16, Martijn van Steenbergen wrote: So here's a totally wild idea Sjoerd and I came up with. What if newtypes were unwrapped implicitly? Subtyping. What advantages and disadvantages would it have? The typechecker being psychic; the fact that it isn't. It's very easy to add forms of subtyping and make a mess of type and instance inference. In what cases would this lead to ambiguous code? If f :: x - ZipList y we get traverse f :: t x - [t y] but it is not clear whether to attach the unpacking to f or to the result, and that will determine the idiom in which the traversal occurs. And that's before you start mixing the sugar of newtypes with the fertiliser of GADTs... But even if it's dangerous to unpack newtypes silently, it's rather nice to do it systematically, via a type class. Here are old posts of mine which mention this and then show off a bit. http://www.mail-archive.com/haskell-cafe@haskell.org/msg37213.html http://www.haskell.org/pipermail/libraries/2008-January/008917.html These days, how about class Newtype n where type Unpack n pack :: Unpack n - n unpack :: n - Unpack n and related machinery? Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Haskell Weekly News: Issue 140 - November 22, 2009
Hi Benjamin On 24 Nov 2009, at 02:35, Benjamin L.Russell wrote: On Sat, 21 Nov 2009 12:14:29 -0800 (PST), jfred...@gmail.com wrote: Typef*ck: Brainf*ck in the type system. Johnny Morrice [23]showed us his implementation of everyone's favorite profane programming language... in the type system. In general, if a programming language-related term contains what is generally regarded as a profane word as a component, for what kinds of written material should I prioritize accuracy vs. propriety? Who gives a brain? More seriously, I worry that inaccuracy (other than blessed relief from tedious pedantry, of course) might ever be improper. Lots of arts academia write learned articles about filth, and it's no big deal when it's in quotation. That's the situation here, no? Perhaps use quotation marks just to be clear that the terminology is not of your making. But you should have no need of ASCII-art fig leaves. (Now, as far as *email* (e.g., HWN) is concerned, it makes sense to act like wise spammers the world over and disguise your true intentions from the automated filters. People from Scunthorpe must be really fed up doing that. I know they're fed up being used as an example, too. Sorry.) Yours ever Coqnor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is proof by testing possible?
On 10 Nov 2009, at 05:52, Curt Sampson wrote: On 2009-11-09 14:22 -0800 (Mon), muad wrote: Proof: True for n = 0, 1, 2, 3, 4 (check!), hence true for all n. QED. ... Actually, the test is that it's true for 0 through 4 is not sufficient for a proof; It's enough testing... you also need to prove in some way that you need do no further tests. ...and you can calculate how much testing is enough by computing an upper bound on the polynomial degree of the expression. (The summation operator increments degree, the difference operator decreases it, like in calculus.) Showing that particular point in this case appears to me to lie outside the realm of testing. You need to appeal to a general theorem about expressions of a particular form, but if that theorem is in the library, the only work you need do is to put the expressions in that form. This is sometimes described as the reflective proof method: express problem in language capturing decidable fragment; hit with big stick. There are lots of other examples of this phenomenon. The zero-one principle for sorting networks is a favourite of mine. I'm sure there's more to be found here. It smells a bit of theorems for free: the strength comes from knowing what you don't. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is () a 0-length tuple?
How about this? {-# LANGUAGE ThinkTotal #-} On 8 Nov 2009, at 09:53, Svein Ove Aas wrote: On Sun, Nov 8, 2009 at 9:52 AM, Ketil Malde ke...@malde.org wrote: Eugene Kirpichov ekirpic...@gmail.com writes: In JavaScript there is a null value, that is the only value of the null type. Isn't () the same thing? The only value of the unary type? No, () has two values: () and undefined (t.i., _|_). () is the only value of (). If we could agree a standard set of email pragmas, we could save ourselves a lot of violent agreement. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative but not Monad
Hi On 31 Oct 2009, at 10:39, Conor McBride wrote: Hi On 30 Oct 2009, at 16:14, Yusaku Hashimoto wrote: Hello cafe, Do you know any data-type which is Applicative but not Monad? [can resist anything but temptation] I have an example, perhaps not a datatype: tomorrow-you-will-know Elaborating, one day later, if you know something today, you can arrange to know it tomorrow if will know a function tomorrow and its argument tomorrow, you can apply them tomorrow but if you will know tomorrow that you will know something the day after, that does not tell you how to know the thing tomorrow Put otherwise, unit-delay is applicative but not monadic. I've been using this to organise exactly what happens when in those wacky miraculous-looking circular programs. It seems quite promising, so far... Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative but not Monad
On 2 Nov 2009, at 00:11, Ross Paterson wrote: On Sun, Nov 01, 2009 at 04:20:18PM +, Conor McBride wrote: On 31 Oct 2009, at 10:39, Conor McBride wrote: I have an example, perhaps not a datatype: tomorrow-you-will-know Elaborating, one day later, if you know something today, you can arrange to know it tomorrow if will know a function tomorrow and its argument tomorrow, you can apply them tomorrow but if you will know tomorrow that you will know something the day after, that does not tell you how to know the thing tomorrow Yes, but if you will know tomorrow that you will know something tomorrow, then you will know that thing tomorrow. That depends on what tomorrow means tomorrow. The applicative does coincide with a monad, just not the one you first thought of (or/max rather than plus). True, but it's not the notion I need to analyse circular programs. I'm looking for something with a fixpoint operator fix :: (Tomorrow x - x) - x which I can hopefully use to define things like repmin :: Tree Int - (Int, Tomorrow (Tree Int)) so that the fixpoint operator gives me a Tomorrow Int which I can use to build the second component, but ensures that the black-hole-tastic Tomorrow (Tomorrow (Tree Int)) I also receive is too late to be a serious temptation. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Applicative but not Monad
Hi On 30 Oct 2009, at 16:14, Yusaku Hashimoto wrote: Hello cafe, Do you know any data-type which is Applicative but not Monad? [can resist anything but temptation] I have an example, perhaps not a datatype: tomorrow-you-will-know Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] better way to do this?
On 7 Oct 2009, at 15:04, John A. De Goes wrote: On Oct 7, 2009, at 3:13 AM, Ketil Malde wrote: Peter Verswyvelen bugf...@gmail.com writes: So yes, without using IO, Haskell forces you into this safe spot One could argue that IO should be broken down into a set of sub- monads encapsulating various subsets of the functionality - file system, network access, randomness, and so on. This could extend the safe spot to cover much more computational real estate, and effectively sandbox programs in various ways. Good idea in theory, in practice I suspect it would lead to unmanageable boilerplate. Aye, but today's boilerplate is tomorrow's language design. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal packages - cabbages
Hi Jason On 22 Sep 2009, at 10:04, Jason Dusek wrote: 2009/09/21 Conor McBride co...@strictlypositive.org: ...or have unpleasant memories of being made to eat sulphurous overboiled cabbage on pain of no pudding. Well, maybe the Cabal cabbages are Napa cabbages or red cabbages or pickled cabbages or Savoy cabbages? Mmm. Kimchi! It is too bad, really, that a wholesome vegetable -- good raw or pickled or in little salady things like coleslaw -- finds itself used as a disincentive. I quite agree. Despite the best efforts of school kitchens, I remain stubbornly enthusiastic for the humble cabbage. In fact, I rather think I'll fetch one for my dinner. I'm just suggesting that the marketing department consider the variety of connotations and suggestions the term evokes before adopting it: legendary backfirings abound (the Spanish sales failure of a car called the nova, for example). And what disturbs me is just how scarily spot-on the wholesome vegetable metaphor turns out to be. The time has come... Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal packages - cabbages
Hi On 22 Sep 2009, at 15:25, D. Manning wrote: 2009/9/22 Conor McBride co...@strictlypositive.org I'm just suggesting that the marketing department consider the variety of connotations and suggestions the term evokes before adopting it: legendary backfirings abound (the Spanish sales failure of a car called the nova, for example). Its not important but the nova story really is legendary: http://www.snopes.com/business/misxlate/nova.asp I chose my words with caution. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal packages - cabbages
On 20 Sep 2009, at 23:11, Jason Dusek wrote: Some day, we're going to need a short, catchy name for Cabal packages. Let's call them cabbages. Not that this is a good reason to change your mind, but some sufficiently ancient Brits may remember a televisual entertainment programme in which kids competed to win prizes by answering questions (one prize per answer) until their arms could no longer contain the prizes and they dropped one. The prize for an incorrect answer was, of course, a cabbage (large, hard to hold on to, symbolic of failed social mobility). Probably the people who associate cabbages with error in this way are few in number. Perhaps larger in number are those who simply fear vegetables, or have unpleasant memories of being made to eat sulphurous overboiled cabbage on pain of no pudding. Cabbage is regarded by many as a punishment, compared to, say, an enviably juicy sheep. It's a mark of inability to afford the aforementioned sheep, or of a kind of holier-than-thou middle class faux-puritanism with pretentions to virtue. +1 Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Cabal packages - cabbages
Hi Jón On 21 Sep 2009, at 10:23, Jon Fairbairn wrote: Conor McBride co...@strictlypositive.org writes: On 20 Sep 2009, at 23:11, Jason Dusek wrote: Some day, we're going to need a short, catchy name for Cabal packages. Let's call them cabbages. Not that this is a good reason to change your mind, but some sufficiently ancient Brits may remember a televisual Speaking of ancient Brits, the Finns used to call Britain cabbage-land, in case that alters anyone's opinion. It's always somewhere else, isn't it? Somehow, a vision of Michael Palin bursting into the RAF officers' mess shouting cabbage crates over the briny! springs to mind. When faced with blank incomprehension and a request to speak English, he replies but I've got to use banter!. Seems that goes for us too. TTFN Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is it possible to prove type *non*-equality in Haskell?
Hi all Interesting stuff. Thanks for this. On 26 Aug 2009, at 03:45, Ryan Ingram wrote: Hi Dan, thanks for the great reply! Some thoughts/questions follow. On Tue, Aug 25, 2009 at 3:39 PM, Dan Doeldan.d...@gmail.com wrote: Well, this isn't surprising; you wouldn't have it even in a more rigorous proof environment. Instead, you'd have to make the return type something like Either (a == b) (a /= b) Yes, and as you see I immediately headed in that direction :) We know by parametricity that contradiction n p isn't inhabited as its type is (forall a. a) But in Haskell, we know that it _is_ inhabited, because every type is inhabited by bottom. And one way to access this element is with undefined. Of course. But it is uninhabited in the sense that if you case analyze on it, you're guaranteed not to reach the RHS of the case. Which is as close to uninhabited as you get in Haskell. I think that's close enough to make uninhabited a useful shorthand. Well, matching against TEq is not going to work. The way you do this in Agda, for instance, is: notZeqS :: forall n - Not (TEq Z (S n)) notZeqS = Contr (\()) Yes, I had seen Agda's notation for this and I think it is quite elegant. Perhaps {} as a pattern in Haskell as an extension? Something of the sort has certainly been suggested before. At the very least, we should have empty case expressions, with at least a warning generated when there is a constructor case apparently possible. [..] But right now it seems that I need to make a separate notEq for each pair of concrete types, which isn't really acceptable to me. Can you think of any way to do so? I think it's likely to be quite tricky, but you might be able to minimize the burden by adapting an old trick (see my thesis, or Eliminating Dependent Pattern Matching by Goguen, McBride, McKinna, or A Few Constructions on Constructors by the same authors). Basically what I want is this function: notEq :: (compiler can prove a ~ b is unsound) = Not (TEq a b) Sadly, I think you are right that there isn't a way to write this in current GHC. Perhaps it's not exactly what you want, but check this out. I've used SHE, but I'll supply the translation so you know there's no cheating. {-# OPTIONS_GHC -F -pgmF she #-} {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts, MultiParamTypeClasses, UndecidableInstances, RankNTypes, EmptyDataDecls #-} module NoConfusion where Some type theorists call the fact that constructors are injective and disjoint the no confusion property, and the fact (?) that they cover the datatype the no junk property. In Haskell, junk there is, but there is strictly no junk. import ShePrelude data Nat :: * where Z :: Nat S :: Nat - Nat deriving SheSingleton The deriving SheSingleton bit makes the preprocessor build the singleton GADT for Nat. From ShePrelude we have type family SheSingleton ty :: * - * and from the above, we get data SheTyZ = SheTyZ data SheTyS x1 = SheTyS x1 type instance SheSingleton (Nat) = SheSingNat data SheSingNat :: * - * where SheWitZ :: SheSingNat (SheTyZ) SheWitS :: forall sha0. SheSingleton (Nat ) sha0 - SheSingNat (SheTyS sha0) Now, let's have newtype Naught = Naught {naughtE :: forall a. a} Thanks to Dave Menendez for suggesting this coding of the empty type. data EQ :: forall (a :: *). {a} - {a} - * where Refl :: EQ a a It may look like I've given EQ a polykind, but after translation, the forall vanishes and the {a}s become *s. My EQ is just the usual thing in * - * - *. OK, here's the trick I learned from Healf Goguen one day in 1997. Define a type-level function which explains the consequences of knowing that two numbers are equal. type family WhatNatEQProves (m :: {Nat})(n :: {Nat}) :: * type instance WhatNatEQProves {Z}{Z}= () type instance WhatNatEQProves {Z}{S n} = Naught type instance WhatNatEQProves {S m} {Z}= Naught type instance WhatNatEQProves {S m} {S n} = EQ m n Those type-level {Z} and {S n} guys just translate to SheTyZ and (SheTyS n), respectively. Now, here's the proof I learned from James McKinna, ten minutes later. noConf :: pi (m :: Nat). pi (n :: Nat). EQ m n - WhatNatEQProves m n noConf m n Refl = noConfDiag m noConfDiag :: pi (n :: Nat). WhatNatEQProves n n noConfDiag {Z} = () noConfDiag {S n} = Refl This pi (n :: Nat). ... is translated to forall n. SheSingleton Nat n - ... which computes to forall n. SheSingNat n - ... The expression-level {Z} and {S n} translate to SheWitZ and (SheWitS n), accessing the singleton family. Preprocessed, we get noConf :: forall m . SheSingleton ( Nat) m - forall n . SheSingleton ( Nat) n - EQ m n - WhatNatEQProves m n noConf m n Refl = noConfDiag m noConfDiag :: forall n . SheSingleton ( Nat) n - WhatNatEQProves n n noConfDiag (SheWitZ) = () noConfDiag (SheWitS n) = Refl James's cunning idea was to match on
Re: [Haskell-cafe] How to convert a list to a vector encoding its length in its type?
Hi I'm sure it won't be to everyone's taste, but here's what SHE makes of this problem. SHE lives here http://personal.cis.strath.ac.uk/~conor/pub/she {-# OPTIONS_GHC -F -pgmF she #-} {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts, MultiParamTypeClasses, RankNTypes #-} You need to turn lots of stuff on to support the coding: it would need much less machinery if this stuff were directly implemented. module Vec where import ShePrelude data Nat :: * where Z :: Nat S :: Nat - Nat deriving (SheSingleton) I'm asking for the generation of the singleton family, so that I can form pi-types over Nat. data Vec :: {Nat} - * - * where VNil :: Vec {Z} x (:) :: x - Vec {n} x - Vec {S n} x Vectors, in the dependently typed tradition. instance Show x = Show (Vec {n} x) where show VNil = VNil show (x : xs) = show x ++ : ++ show xs I gather I won't need to roll my own, next version. listVec :: [a] - (pi (n :: Nat). Vec {n} a - t) - t listVec [] f = f {Z} VNil listVec (x : xs) f = listVec xs (\ n ys - f {S n} (x : ys)) And that's your gadget: it gives you the length and the vector. *Vec listVec Broad (const show) listVec Broad (const show) 'B' : 'r' : 'o' : 'a' : 'd' : VNil If you're curious, here's what SHE generates for the above. {-# OPTIONS_GHC -F -pgmF she #-} {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts, MultiParamTypeClasses, RankNTypes #-} module Vec where import ShePrelude data Nat :: * where Z :: Nat S :: Nat - Nat data Vec :: * - * - * where VNil :: Vec (SheTyZ) x (:) :: x - Vec (n) x - Vec (SheTyS n) x instance Show x = Show (Vec (n) x) where show VNil = VNil show (x : xs) = show x ++ : ++ show xs listVec :: [a] - (forall n . SheSingleton ( Nat) n - Vec (n) a - t) - t listVec [] f = f (SheWitZ) VNil listVec (x : xs) f = listVec xs (\ n ys - f (SheWitS n) (x : ys)) data SheTyZ = SheTyZ data SheTyS x1 = SheTyS x1 data SheTyVNil = SheTyVNil data (:$#$#$#:) x1 x2 = (:$#$#$#:) x1 x2 type instance SheSingleton (Nat) = SheSingNat data SheSingNat :: * - * where SheWitZ :: SheSingNat (SheTyZ) SheWitS :: forall sha0. SheSingleton (Nat ) sha0 - SheSingNat (SheTyS sha0) instance SheChecks (Nat ) (SheTyZ) where sheTypes _ = SheWitZ instance SheChecks (Nat ) sha0 = SheChecks (Nat ) (SheTyS sha0) where sheTypes _ = SheWitS (sheTypes (SheProxy :: SheProxy (Nat ) (sha0))) All good clean fun Conor On 21 Aug 2009, at 17:18, Daniel Peebles wrote: I'm pretty sure you're going to need an existential wrapper for your fromList function. Something like: data AnyVector a where AnyVector :: Vector a n - AnyVector a because otherwise you'll be returning different types from intermediate iterations of your fromList function. I was playing with n-ary functions yesterday too, and came up with the following, which doesn't need undecidable instances, if you're interested: type family Replicate n (a :: * - *) b :: * type instance Replicate (S x) a b = a (Replicate x a b) type instance Replicate Z a b = b type Function n a b = Replicate n ((-) a) b (you can also use the Replicate function to make type-level n-ary vectors and maybe other stuff, who knows) Hope this helps, Dan On Fri, Aug 21, 2009 at 7:41 AM, Bas van Dijkv.dijk@gmail.com wrote: Hello, We're working on a Haskell binding to levmar[1] a C implementation of the Levenberg-Marquardt optimization algorithm. The Levenberg-Marquardt algorithm is an iterative technique that finds a local minimum of a function that is expressed as the sum of squares of nonlinear functions. It has become a standard technique for nonlinear least-squares problems. It's for example ideal for curve fitting. The binding is nearly finished and consists of two layers: a low- level layer that directly exports the C bindings and a medium-level layer that wraps the lower-level functions and provides a more Haskell friendly interface. The Medium-Level (ML) layer has a function which is similar to: levmarML :: (a - [Double] - Double) - [Double] - [(a, Double)] - [Double] levmarML model initParams samples = ... So you give it a model function, an initial guess of the parameters and some input samples. levmarML than tries to find the parameters that best describe the input samples. Of course, the real function has more arguments and return values but this simple version will do for this discussion. Al-dough this medium-level layer is more Haskell friendly than the low-level layer it still has some issues. For example a model function is represented as a function that takes a list of parameters. For example: \x [p1, p2, p3] - p1*x^2 + p2*x + p3 You have to ensure that the length of the initial guess of parameters is exactly 3. Otherwise you get run-time pattern-match failures. So I would like to create a new High-Level (HL) layer that overcomes this problem. First
Re: DDC compiler and effects; better than Haskell? (was Re: [Haskell-cafe] unsafeDestructiveAssign?)
Hi Dan On 12 Aug 2009, at 22:28, Dan Doel wrote: On Wednesday 12 August 2009 10:12:14 am John A. De Goes wrote: I think the point is that a functional language with a built- in effect system that captures the nature of effects is pretty damn cool and eliminates a lot of boilerplate. It's definitely an interesting direction (possibly even the right one in the long run), but it's not without its faults currently (unless things have changed since I looked at it). From what I've seen, I think we should applaud Ben for kicking the open here. Is Haskell over-committed to monads? Does Haskell make a sufficient distinction between notions of value and notions of computation in its type system? For instance: what effects does disciple support? Mutation and IO? What if I want non-determinism, or continuations, etc.? How do I as a user add those effects to the effect system, and specify how they should interact with the other effects? As far as I know, there aren't yet any provisions for this, so presumably you'll end up with effect system for effects supported by the compiler, and monads for effects you're writing yourself. By contrast, monad transformers (for one) let you do the above defining of new effects, and specifying how they interact (although they're certainly neither perfect, nor completely satisfying theoretically). Someone will probably eventually create (or already has, and I don't know about it) an extensible effect system that would put this objection to rest. Until then, you're dealing in trade offs. It's still very much on the drawing board, but I once flew a kite called Frank which tried to do something of the sort (http://cs.ioc.ee/efftt/mcbride-slides.pdf). Frank distinguishes value types from computation types very much in the manner of Paul Blain Levy's call-by-push-value. You make a computation type from a value type v by attaching a capabilty to it (a possibly empty set of interfaces which must be enabled) [i_1,..i_n]v. You make a value type from a computation type c by suspending it {c}. Expressions are typed with value components matched up in the usual way and capabilities checked for inclusion in the ambient capability. That is, you don't need idiom-brackets because you're always in them: it's just a question of which idiom, as tracked by type. There's a construct to extend the ambient idiom by providing a listener for an interface (subtly disguised, a homomorphism from the free monad on the interface to the outer notion of computation). Listeners can transform the value type of the computations they interpret: a listener might offer the throw capability to a computation of type t, and deliver a pure computation of type Maybe t. But [Throw]t and []Maybe t are distinguished, unlike in Haskell. Moreover {[]t} and t are distinct: the former is lazy, the latter strict, but there is no reason why we should ever evaluate a pure thunk more than once, even if it is forced repeatedly. I agree with Oleg's remarks, elsewhere in this thread: there is a middle ground to be found between ML and Haskell. We should search with open minds. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: DDC compiler and effects; better than Haskell? (was Re: [Haskell-cafe] unsafeDestructiveAssign?)
On 12 Aug 2009, at 20:40, Don Stewart wrote: bugfact: Well, the point is that you still have monadic and pure programming styles. It's true that applicative style programming can help here, but then you have these $ and * operators everywhere, which also feels like boilerplate code (as you mention, some extensions could help here) Overloading whitespace as application in the Identity idiom! :) [cough!] Conor psst: http://personal.cis.strath.ac.uk/~conor/pub/she/idiom.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is closing a class this easy?
Hi Miguel On 18 Jul 2009, at 07:58, Miguel Mitrofanov wrote: Oops... Sorry, wrong line. Should be isAB :: forall p. p A - p B - p x Yep, dependent case analysis, the stuff of my thesis,... On 18 Jul 2009, at 10:51, Miguel Mitrofanov wrote: What is it for? I have a different purpose in mind. I want to write localize :: (forall a. Equipment a = Abstract a) - Concrete rather than localize :: (forall a. F1 a - ... - Fn a - Abstract a) - Concrete so I can use the type class machinery to pass around the dictionaries of equipment. I want to make sure that nobody else gets the equipment. It's possible that I don't need to be so extreme: it's enough that there's no other way to use Abstracts than via localize. Yes, you would know that only A and B are Public, but you have no way of telling that to the compiler. I usually prefer something like that: class Public x where blah :: ... isAB :: forall y. (A - y) - (B - y) - x - y But now I can write bogus instances of Public with genuine implementations of blah and wicked lies for isAB. It is important to use the dependent version, otherwise I might have instance Public (A, B) where isAB af bf (a, b) = af a and lots more, without even lying. Both solutions, however, allow the user to declare some new instances when GeneralizedNewtypeDeriving is enabled. I'm scared. What about this? data EQ :: * - * - * where Refl :: EQ x x class Public x where blah :: EQ x Fred instance Public Fred where blah = Refl What happens when I say newtype Jim = Hide Fred deriving Public ? I tried it. I get blah :: EQ Jim Fred It's clear that GeneralizedNewtypeDeriving goes too far. I hope a class with *no* instances in public has no newtype leak! Fun stuff. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] is closing a class this easy?
On 18 Jul 2009, at 01:43, Lennart Augustsson wrote: As far as I know it works. It's an old Oleg trick. Then it probably does work. The only drawback is that error messages may refer to Private. As I found out when probing its security. No instance for Moo.Private shows up. I guess that's what happens when you hide stuff: you get told what stuff's being hidden. In some situations, that's insecure, but here it's ok. Cheers (and have fun in China, Lennart!) Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
newtype deriving, was Re: [Haskell-cafe] is closing a class this easy?
Hi Stefan On 18 Jul 2009, at 09:42, Stefan Holdermans wrote: Conor, What happens when I say newtype Jim = Hide Fred deriving Public ? I tried it. I get blah :: EQ Jim Fred It's clear that GeneralizedNewtypeDeriving goes too far. Now, I am scared. This should be regarded as a bug in generalised newtype deriving, shouldn't it? I would expect newtype deriving to be unable to come up with instances that cannot be written by hand. I think the latter is a useful general principle for deriving. The trouble here is that somewhere along the line (GADTs? earlier?) it became possible to construct candidates for p :: * - * which don't respect isomorphism. These tend to be somewhat intensional in nature, and they mess up the transfer of functionality. If we could be sure that all such a p would do with its parameter (x, say) is trade in values of x (as opposed to trading in the identity of x), then we could be sure that p respects isomorphisms. I'm hoping that a category theorist will say something about dinaturality at this point, because I'd like to understand that stuff. I wonder if there's a potential refinement of the kind system lurking here, distinguishing *, types-up-to-iso, from |*|, types-up-to-identity. That might help us to detect classes for which newtype deriving is inappropriate: GADTs get indexed over |*|, not *; classes of *s are derivable, but classes of |*|s are not. I certainly don't have a clear proposal just now. It looks like an important distinction: recognizing it somehow might buy us something. I would have expected people out on the streets marching to GHC headquarters by now; how can you stay so calm? GHC HQ are up to their armpits in newtypes already. This distinction between type equality and (trivial) type isomorphism is something they're already facing. I don't know if they've solved this problem yet, but I suspect they're in the area. No need for a commotion. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: newtype deriving, was Re: [Haskell-cafe] is closing a class this easy?
Hi Wolfgang On 18 Jul 2009, at 13:42, Wolfgang Jeltsch wrote: Am Samstag, 18. Juli 2009 11:43 schrieb Conor McBride: The trouble here is that somewhere along the line (GADTs? earlier?) it became possible to construct candidates for p :: * - * which don't respect isomorphism. Hello Conor, I’m not sure whether I exactly understand what you mean here. I think, it’s the following: Say, you have a type A and define a type B as follows: newtype B = B A Then, for any p :: * - *, the type p A should be isomorphic to p B, i.e., it should basically contain the same values. This is no longer true with GADTs since you can define something like this: data GADT a where GADT :: GADT A Now, GADT :: GADT A but not GADT :: GADT B. Is this what you mean? Yes, that's what I mean. These tend to be somewhat intensional in nature, and they mess up the transfer of functionality. Could you maybe elaborate on this? Just as you've shown, we can use GADTs to express a p such that p A is inhabited but p B is not(*) Moreover, we can write type families which make TF A = IO String TF B = String so it'd be better not to get A and B confused. But all of these nasties rely on taking an intensional view of types as pieces of syntax, rather than the extensional view of types as sets of values. Predicates (to use a Curry-Howardism) which rely only on the extensional properties of types can be relied upon to respect isomorphism, and indeed to respect trivial isomorphisms trivially. (You can refine this to *inclusion* if you pay attention to co/contra-variance. This would give us inflate :: Functor f = f Void - f x as a no-op.) Your GADT is an intensional predicate --- being A, rather than having the values of A --- so it respects fewer equations. Consider a type expression t[x], over a free type variable x. Suppose you have some f :: a - b and g :: b - a. For the most part, you can use these to construct t[f,g :: t[a] - t[b] and hence t[g,f :: t[b] - t[a] by recursion on the structure of t. E.g,, x[f, g = f Bool[f, g = id (s - t)[f, g = \ h - t[f,g . h . s[g,f ... You'll find that t[id,id = id. But you'll get stuck at GADTs and type families. Functions both ways don't give you enough information: you need equality (same objects, different morphisms). Type classes are predicates: supporting a dictionary. If they happen to be extensional predicates, then they should support newtype deriving. Can we draw out this distinction somehow? Interesting place to go... Cheers Conor (*) usual caveats for bottom spotters ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] is closing a class this easy?
Friends Is closing a class this easy? -- module Moo ( Public(..) ) where class Private x = Public x where blah :: ... class Private x where instance Private A where instance Public A where blah = ... instance Private B where instance Public B where blah = ... -- Modules importing Moo get Public and its instances, but cannot add new ones: any such instances must be accompanied by Private instances, and Private is out of scope. Does this work? If not, why not? If so, is this well known? It seems to be just what I need for a job I have in mind. I want a class with nothing but hypothetical instances. It seems like I could write -- module Noo ( Public(..) , public ) where class Private x = Public x where blah :: ... blah = ... class Private x where public :: (forall x. Public x = x - y) - y public f = f Pike data Pike = Pike instance Private Pike instance Public Pike -- But if I don't tell 'em Pike, I've ensured that blah can only be used in the argument to public. Or is there a hole? Cures youriously Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non Empty List?
Hi folks data NE x = x : Maybe (NE x) ? It's Applicative in at least four different ways. Can anyone find more? Conor On 5 Jun 2009, at 01:34, Edward Kmett wrote: Günther, Miguel had the easiest suggestion to get right: Your goal is to avoid the redundant encoding of a list of one element, so why do you need to get rid of the Many a [] case when you can get rid of your Single a case! module NE where import Prelude hiding (foldr, foldl, foldl1, head, tail) import Data.Foldable (Foldable, foldr, toList, foldl, foldl1) import Data.Traversable (Traversable, traverse) import Control.Applicative data NE a = NE a [a] deriving (Eq,Ord,Show,Read) Now we can fmap over non-empty lists instance Functor NE where fmap f (NE a as) = NE (f a) (map f as) It is clear how to append to a non-empty list. cons :: a - NE a - NE a a `cons` NE b bs = NE a (b:bs) head is total. head :: NE a - a head (NE a _) = a tail can return an empty list, so lets model that tail :: NE a - [a] tail (NE _ as) = as We may not be able to construct a non-empty list from a list, if its empty so model that. fromList :: [a] - Maybe (NE a) fromList (x:xs) = Just (NE x xs) fromList [] = Nothing We can make our non-empty lists an instance of Foldable so you can use Data.Foldable's versions of foldl, foldr, etc. and nicely foldl1 has a very pretty total definition, so lets use it. instance Foldable NE where foldr f z (NE a as) = a `f` foldr f z as foldl f z (NE a as) = foldl f (z `f` a) as foldl1 f (NE a as) = foldl f a as We can traverse non-empty lists too. instance Traversable NE where traverse f (NE a as) = NE $ f a * traverse f as And they clearly offer a monadic structure: instance Monad NE where return a = NE a [] NE a as = f = NE b (bs ++ concatMap (toList . f) as) where NE b bs = f a and you can proceed to add suitable instance declarations for it to be a Comonad if you are me, etc. Now a singleton list has one representation NE a [] A list with two elements can only be represented by NE a [b] And so on for NE a [b,c], NE 1 [2..], etc. You could also make the data Container a = Single a | Many a (Container a) definition work that Jake McArthur provided. For the category theory inspired reader Jake's definition is equivalent to the Cofree comonad of the Maybe functor, which can encode a non-empty list. I leave that one as an exercise for the reader, but observe Single 1 Many 1 (Single 2) Many 1 (Many 2 (Single 3)) And the return for this particular monad is easy: instance Monad Container where return = Single In general Jake's non-empty list is a little nicer because it avoids a useless [] constructor at the end of the list. -Edward Kmett On Thu, Jun 4, 2009 at 5:53 PM, GüŸnther Schmidt gue.schm...@web.de wrote: Hi, I need to design a container data structure that by design cannot be empty and can hold n elements. Something like a non-empty list. I started with: data Container a = Single a | Many a [a] but the problem above is that the data structure would allow to construct a Many 5 [] :: Container Int. I can't figure out how to get this right. :( Please help. Günther ___ 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
[Haskell-cafe] web musing
Comrades I'm in a perplexing situation and I'd like to appeal to the sages. I've never written anything other than static HTML in my life, and I'd like to make a wee web service: I've heard some abbreviations, but I don't really know what they mean. I've got a function (possibly the identity, possibly const , who knows?) assistant :: String - String and I want to make a webpage with an edit box and a submit button. If I press the submit button with the edit box containing string s, I'd like the page to reload with the edit box reset to (assistant s). Will I need to ask systems support to let me install some haskelly sort of web server? Looks likely, I suppose. In general, what's an easy way to put a web front end on functionality implemented in Haskell? Hoping this isn't a hard question Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: new version of uu-parsinglib
On 31 May 2009, at 20:40, S. Doaitse Swierstra wrote: A new version of the uu-parsinglib has been uploaded to hackage. It is now based on Control.Applicative where possible. It's mutual. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Free theorems for dependent types?
Hi On 20 May 2009, at 07:08, Eugene Kirpichov wrote: Thanks for the thorough response. I've found BarrasBernardo's work (at least, slides) about ICC*, I'll have a look at it. Could you provide with names of works by Altenkirch/Morris/Oury/you? The unordered pair example was especially interesting, since I am somewhat concerned with which operations do not break parametricity for *unordered sets* (as opposed to lists) - turns out, not too many. Unordered sets or bags? Both are interesting, but hiding multiplicity makes sets tricky. Anyway, the news on publications is not so good. There's a paper Observational Equality, Now! by Altenkirch, McB, Swierstra which describes more or less how we handle observational equalities in general, but the specific instantiation of that pattern to quotients is more recent. An older paper Constructing Polymorphic Programs with Quotient Types by Abbott, Altenkirch, McB, Ghani extends container theory to things which are fuzzy about position (bags, cycles, etc), so may have some relevance. One formulation of quotients in Epigram 2, by the aforementioned Altenkirch, Morris, McB, Oury, are sadly documented only by the source code of the implementation, which you can find here http://www.e-pig.org/darcs/epigram/src/Quotient.lhs if you're curious. We knocked that up in about half an hour one afternoon shortly before the money ran out. The basic idea is terribly simple. A quotient is an abstract type X/f wrapping a carrier set X which has a notion of normal form given by f : X - Y, for some Y. (e.g. f might be even, and Y Bool, giving arithmetic modulo 2). Equality on X/f is just equality at Y of whatever f gives on the packed C values. You can almost unpack X/f freely, gaining access to the element of the carrier, applying any (possibly dependent) function g you like to it -- just as long as you can prove that forall x x'. f x == f x' - g x == g x' Any such g on X readily lifts to X/f. This to design and redesign an interface of quotient-respecting functions and then work compositionally. Amusingly, under certain circumstances, the idea of quotient by an equivalence fits this picture: given R : X - X - Prop, just take Y, above, to be X - Prop (a predicate describing an equivalence class; predicates are equal by mutual inclusion). That allows you permutative quotients which don't admit a more concrete normal form, like general unordered pairs. Of course, if you do have an order on the data, you can just take f to be sort! Sorry for lack of writings, for which this status dump is poor compensation. Things aren't very applied yet, but the machinery for restricting observation in exchange for guarantees is on its way. We'll see what the summer brings. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Free theorems for dependent types?
Hi Questions of parametricity in dependent types are made more complex by the way in which the Pi-type (x : S) - T corresponds to universal quantification. It's good to think of this type as a very large product, tupling up individual T's for each possible x you can distinguish by observation. For all x here means For each individual x. By contrast, your typical universally quantified type forall x. t gives you fantastic guarantees of ignorance about x! It's really a kind of intersection. For all x here means For a minimally understood x --- your program should work even when x is replaced by a cardboard cutout rather than an actual whatever-it-is, and this guarantees the uniformity of operation which free theorems exploit. I'm reminded of the Douglas Adams line We demand rigidly defined areas of doubt and uncertainty.. In the dependent case, how much uniformity you get depends on what observations are permitted on the domain. So what's needed, to get more theorems out, is a richer language of controlled ignorance. There are useful developments: (1) Barras and Bernardo have been working on a dependent type system which has both of the above foralls, but distinguishes them. As you would hope, the uniform forall, its lambda, and application get erased between typechecking and execution. We should be hopeful for parametricity results as a consequence. (2) Altenkirch, Morris, Oury, and I have found a way (two, in fact, and there's the rub) to deliver quotient structures, which should allow us to specify more precisely which observations are available on a given set. Hopefully, this will facilitate parametric reasoning --- if you can only test this, you're bound to respect that, etc. My favourite example is the recursion principle on *unordered* pairs of numbers (N*N/2). uRec : (P : N*N/2 - Set) - ((y : N) - P (Zero, y)) - ((xy : N*N/2) - P xy - P (map Suc xy)) - (xy : N*N/2) - P xy Given an unordered pair of natural numbers, either one is Zero or both are Suc, right? You can define some of our favourite operators this way. add = uRec (\ _ - N) (\ y - y) (\ _ - Suc . Suc) max = uRec (\ _ - N) (\ y - y) (\ _ - Suc) min = uRec (\ _ - N) (\ y - y) (\ _ - id) (==) = uRec (\ _ - Bool) isZero (\ _ - id) I leave multiplication as an exercise. The fact that these operators are commutative is baked into their type. To sum up, the fact that dependent types are good at reflection makes them bad at parametricity, but there's plenty of work in progress aimed at the kind of information hiding which parametricity can then exploit. There are good reasons to be optimistic here. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] conflicting variable definitions in pattern
On 16 May 2009, at 03:54, wren ng thornton wrote: Conor McBride wrote: Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway) But unification is what you get by adding non-linearity. Hang on a minute: we're solving for sb in sb(p)=v not in sb(s)=sb(t)... Sure, all terms are ground; ...which makes it a rather special and degenerate and unawesome case of unification: the kind of unification you don't need a unification algorithm to solve. would you prefer I said testing for membership in an element of the RATEG class? I'm not familiar with that terminology, but I'll check out the link. For more ickiness about RATEG, it's not closed under compliment and the emptiness problem is undecidable (so dead code elimination can't always work). Even restricting to the closed subset (aka tree- automata with (dis-)equality constraints) leaves emptiness undecidable, though there are a couple still more restricted classes that are decidable. cf ch.4 of TATA http://tata.gforge.inria.fr/ Let's be clear. The suggestion is only that a slightly more compact notation be permitted for functionality already available via guards or view patterns. It cannot introduce any dead code elimination problems which are not already present. I'm sorry, but I just don't see the bogeyman here. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] conflicting variable definitions in pattern
Hi On 15 May 2009, at 09:11, Sittampalam, Ganesh wrote: Martin Hofmann wrote: It is pretty clear, that the following is not a valid Haskell pattern: foo (x:x:xs) = x:xs My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term. That's what my daddy did in 1970. It was an extension of LISP with pattern matching. He used EQUAL. That makes me one of the few functional programmers who's had this feature taken away from them. I'm not weeping, but I do miss it. How do you define the same term? One natural way of compiling it would be to foo (x:y:xs) | x == y = x:xs but then pattern matching can introduce Eq constraints which some might see as a bit odd. Doesn't seem that odd to me. Plenty of other language features come with constraints attached. Isn't this allowed, because this would require a strict evaluation of the 'x' variables? The translation into == would probably introduce some strictness, for most implementations of Eq. I don't think this is a huge problem in itself. There's some conceptual ugliness in that such a mechanism *relies* on fall-through. In principle a sequence of guardless patterns can always be fleshed out (at some cost) to disjoint patterns. What precisely covers the case disjoint from (x, x)? This is fixable if one stops quibbling about guardlessness, or even if one adds inequality patterns. One certainly needs a convention about the order in which things happen: delaying equality tests until after constructor matching --- effectively the guard translation --- seems sensible and preserves the existing compilation regime. Otherwise, repeated pattern variables get (==)-tested, linear ones are lazy. Meanwhile, yes the semantics depends on the implementation of (==), but what's new? That's true of do too. The guard translation: linearize the pattern, introducing new vars for all but the leftmost occurrence of repeated vars. For each new x' made from x, add a guard x == x'. The new guards should come in the same order as the new variables and stand before any other guards present. Presumably one can already cook up an ugly version of this with view patterns ((x ==) - True). It seems to me that the only questions of substance remaining is whether improved clarity in normal usage is worth a little more translational overhead to unpick what's wrong when weird things happen, and whether any such gain is worth the effort in implementation. I miss lots of stuff from when I was a kid. I used to write elem x (_ ++ x : _) = True elem _ _ = False and think that was cool. How dumb was I? Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] conflicting variable definitions in pattern
On 15 May 2009, at 12:07, Lennart Augustsson wrote: In the original language design the Haskell committee considered allowing multiple occurrences of the same variable in a pattern (with the suggested equality tests), but it was rejected in favour of simplicity. Simplicity for whom, is the question? My point is only that there's no technical horror to the proposal. It's just that, given guards, the benefit (in simplicity of program comprehension) of nonlinear patterns over explicit == is noticeable but hardly spectacular. Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway) are wide of the mark. This is just an ordinary cost-versus-benefit issue. My guess is that if this feature were already in, few would be campaigning to remove it. (By all means step up and say why!) As it's not in, it has to compete with other priorities: I'm mildly positive about nonlinear patterns, but there are more important concerns. Frankly, the worst consequence I've had from Haskell's pattern linearity was just my father's derision. He quite naturally complained that his programs had lost some of their simplicity. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] applicative challenge
Hi Thomas This is iffy versus miffy, a standard applicative problem. When you use the result of one computation to choose the next computation (e.g., to decide whether you want to keep doing-and-taking), that's when you need yer actual monad. It's the join of a monad that lets you compute computations. The applicative interface does not allow any interference between the value and computation layers. It's enough for effects which facilitate but do not determine the flow of computation (e.g. threading an environment, counting how often something happens, etc...). So, you ask a sensible... On 4 May 2009, at 22:15, Thomas Hartman wrote: {-# LANGUAGE NoMonomorphismRestriction #-} import Data.List import Control.Monad import Control.Applicative -- Can the function below be tweaked to quit on blank input, provisioned in the applicative style? -- which function(s) needs to be rewritten to make it so? -- Can you tell/guess which function(s) is the problem just by looking at the code below? -- If so, can you explain what the strategy for doing so is? ...nostril question. notQuiteRight = takeWhile (not . blank) $ ( sequence . repeat $ echo ) ^^^ Here, we're doing all the computations, then post-processing the values with a pure function. There's no way the pure function can tell the computation to stop bothering. echo = do l - getLine putStrLn l return l -- this seems to work... is there a way to make it work Applicatively, with lifted takeWhile? seemsToWork = sequenceWhile_ (not . blank) (repeat echo) sequenceWhile_ p [] = return () sequenceWhile_ p (mx:mxs) = do x - mx if p x ^^^ Here, you're exactly using the result of a computation to choose which computations come next. That's a genuinely monadic thing to do: miffy not iffy. then do sequenceWhile_ p mxs else return () If you're wondering what I'm talking about, let me remind/inform you of the definitions. iffy :: Applicative a = a Bool - a t - a t - a t iffy test yes no = cond $ test * yes * no where cond b y n = if b then y else n miffy :: Monad m = m Bool - m t - m t - m t miffy test yes no = do b - test if b then yes else no Apologies for slang/pop-culture references, but iffy means dubious, questionable, untrustworthy miffy is a cute Dutch cartoon character drawn by Dick Bruna The effect of iffy askPresident launchMissiles seekUNResolution is to ask the President, then launch the missiles, then lobby the UN, then decide that the result of seeking a UN resolution is preferable. Remember folks: Missiles need miffy! Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: applicative challenge
Hi Achim On 5 May 2009, at 01:26, Achim Schneider wrote: Conor McBride co...@strictlypositive.org wrote: Remember folks: Missiles need miffy! H. Iff you have something like CoPointed or Foldable, you can thread your own, Applicative, tail back into yourself and decide what you are by inspecting it. Yeah, Applicative on its own is kind of effects without control, or in Lindley-Wadler-Yallop parlance oblivious. The fun starts when you just chuck in a little bit more. Copointed might be overdoing it. Even Alternative gives you quite a lot of control, without going as far as Monad. That makes foldr the join of Hask itself, or something. Bear with me, I'm merely attempting to delurk our resident category theorists by giving them headaches. Good luck Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] types and braces
Hi folks In search of displacement activity, I'm trying to tweak Language.Haskell.Exts to support a few more perfidious Exts I have in mind -- they only need a preprocessor, but I do need to work on parsed programs, ideally. I was hoping to add a production to the grammar of types to admit expressions, delimited by braces: { exp } The idea is that instead of writing, (er, hi Claus), data True data False one just re-uses yer actual Bool (which becomes kind {Bool}) and writes {True} or {False}. The trouble is, the production I've added causes a reduce/reduce conflict in the grammar, but I don't get any more precise complaint than that. I guess what I'd like to know is whether I just need to debug my grammar extension, or whether the notation I'm proposing actually introduces a serious ambiguity that I'm too dim to notice. I'm mostly sending this in the hope that I have one of those d'oh moments you sometimes get when you articulate a stupid question in public. Put me out of my misery, please... Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] types and braces
On 15 Apr 2009, at 16:01, Lennart Augustsson wrote: I'd suggest using some different kind of brackets to relieve the misery, like {| |}. That would speed up my tinkering, certainly. I did have a d'oh moment: you can write data Foo = Moo {goo :: Int} -- braces where a type goes and indeed, commenting out field declarations makes happy happy. However, these { exp } guys never stand as types of things, only as parameters of types, so it might be possible to resolve the problem without fat brackets. Whether it's worth it is another matter... Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] types and braces
Hi Niklas Good to hear from you, and thanks for providing such a useful starting point for my experiments. On 15 Apr 2009, at 19:27, Niklas Broberg wrote: Hi Conor, Conor McBride: The trouble is, the production I've added causes a reduce/reduce conflict in the grammar, but I don't get any more precise complaint than that. To get more precise complaints, you should give the -i flag to happy, that will cause happy to print the whole parser table into a file named Parser.info. It also tells you in which states the conflicts occur, allowing you to track 'em down. So that's how you do it! I was expecting that some such thing would exist. I guess what I'd like to know is whether I just need to debug my grammar extension, or whether the notation I'm proposing actually introduces a serious ambiguity that I'm too dim to notice. I'm mostly sending this in the hope that I have one of those d'oh moments you sometimes get when you articulate a stupid question in public. I don't immediately see what the clash in that context would be - I *think* what you propose should be doable. I'd be interested to know what you come up with, or I might have a look at it myself when I find a few minutes to spare. I've found that I can add a production atype :: { Type } ... | '{' trueexp '}' if I remove the productions for record declarations constr1 :: { ConDecl } | con '{' '}' { RecDecl $1 [] } | con '{' fielddecls '}'{ RecDecl $1 (reverse $3) } which suggests that it is indeed the syntax data Moo = Foo {goo :: Boo Hoo} which is in apparent conflict with my proposed extension. The current parser uses the type parser btype to parse the initial segment of constructor declarations, so my change causes trouble. Further trouble is in store from infix constructors data Noo = Foo {True} :*: Foo {False} should make sense, but you have to look quite far to distinguish that from a record. So I don't see that my proposed extension introduces a genuine ambiguity, but it does make the parser a bit knottier. I can use (|...|) as the brackets I need in the meantime, without even disturbing the lexer, but I'd much rather use {...} if I can learn a bit more happy hacking. My efforts so far have been clumsy and frustrating, but -i might help me see what I'm doing wrong. Subtle stuff Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
Hi On 18 Mar 2009, at 15:00, Conal Elliott wrote: I use these defs: -- | Lift proof through a unary type constructor liftEq :: a :=: a' - f a :=: f a' liftEq Refl = Refl -- | Lift proof through a binary type constructor (including '(,)') liftEq2 :: a :=: a' - b :=: b' - f a b :=: f a' b' liftEq2 Refl Refl = Refl -- | Lift proof through a ternary type constructor (including '(,,)') liftEq3 :: a :=: a' - b :=: b' - c :=: c' - f a b c :=: f a' b' c' liftEq3 Refl Refl Refl = Refl Makes you want kind polymorphism, doesn't it? Then we could just have (=$=) :: f :=: g - a :=: b - f a :=: g b Maybe the liftEq_n's are the way to go (although we called them resp_n when I was young), but they don't work for higher kinds. An alternative ghastly hack might be data PackT2T (f :: * - *) (=$=) :: (PackT2T f :=: PackT2T g) - (a :=: b) - (f a :=: g b) Refl =$= Refl = Refl But now you need a packer and an application for each higher kind. Or some bonkers type-level programming. This one will run and run... Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
Hi On 17 Mar 2009, at 21:06, David Menendez wrote: 2009/3/17 Luke Palmer lrpal...@gmail.com: Here are the original definition and the proofs of comm and trans. Compiles fine with GHC 6.10.1. data (a :=: a') where Refl :: a :=: a comm :: (a :=: a') - (a' :=: a) comm Refl = Refl trans :: (a :=: a') - (a' :=: a'') - (a :=: a'') trans Refl Refl = Refl These two theorems should be in the package. How about this? instance Category (:=:) where id = Refl Refl . Refl = Refl That and the identity-on-objects functor to sets and functions. Mutter mutter Leibniz Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type equality proof
On 17 Mar 2009, at 21:44, Martijn van Steenbergen wrote: Conor McBride wrote: instance Category (:=:) where id = Refl Refl . Refl = Refl That and the identity-on-objects functor to sets and functions. Not sure what you mean by this, Conor. Can you please express this in Haskell code? Apologies for being glib and elliptic: filthy habit. That would be coerce :: (a :=: b) - (a - b) coerce Refl a = a taking arrows in the :=: category (aka the discrete category on *) to arrows in the - category, preserving the objects involved. It captures the main useful consequence of an equation between types. I guess the other thing you need is resp :: (a :=: b) - (f a :=: f b) resp Refl = Refl (any type constructor gives you a functor from the :=: category to itself). If you compose the two, you get Leibniz's characterization of equality -- that it's substitutive: subst :: a :=: b - (f a - f b) subst = coerce . resp Or you can start from subst and build the other two by careful instantiation of f. By the way, I see the motivation for your Eq1 class, which seems useful for the singleton GADTs which get used to give value-level representations to type-level stuff (combine with fmap coerce to get SYB-style cast), but I'm not quite sure where Eq2, etc, come in. Have you motivating examples for these? It's well worth striving for some sort of standard kit here. I should add that mentioning equality is the best way to start a fight at a gathering of more than zero type theorists. But perhaps there are fewer things to cause trouble in Haskell. So thanks for this, Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Henning On 14 Mar 2009, at 01:36, Henning Thielemann wrote: On Tue, 10 Mar 2009, Conor McBride wrote: Apologies for crossposting. Please forward this message to individuals or lists who may be interested. In addition to the recently advertised PhD position at Strathclyde on Reusability and Dependent Types, I am delighted to advertise the following PhD opportunity. {- -- Haskell Types with Numeric Constraints -} Sounds like it could simplify http://hackage.haskell.org/cgi-bin/hackage-scripts/package/ dimensional/ Hope so. a lot. However, isn't this halfheartedly since we all wait for full dependent types? :-) Rome wasn't burnt in a day. Of course I want more than just numerical indexing (and I even have a plan) but numeric constraints are so useful and have so much of their own peculiar structure that they're worth studying in their own right, even for languages which do have full dependent types, let alone Haskell. We'll carry out this project with an eye to the future, to make sure it's compatible with full dependent types. Be assured (excited, nervous, etc...) that this is not halfhearted: it's a wholehearted start. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Wolfgang On 14 Mar 2009, at 12:00, Wolfgang Jeltsch wrote: Am Samstag, 14. März 2009 08:19 schrieb Peter Verswyvelen: Well, in C++ one can already use the numerical values with templates for achieving a lot of compile time computations. So I would be very happy to have this feature in Haskell. It might also be good research towards full dependent types no? I doubt that it will be a good thing to include full dependent types into a language with partial functions like Haskell. I think we could manage quite a bit, though. It seems reasonable to allow types to contain expressions drawn from a total fragment of the value language. Even a tiny fragment (such the expressions built only from fully applied constructors and variables) would be a useful start (vector head, tail, zip, but not vector append). The present capacity for open type functions suggests that it shouldn't be too violent to add some total value-functions (probably with a flag allowing self-certification of totality). We should also ask what the problem is with partiality? I'd far rather have a simplistic Set-based intuition about what values in types might mean, rather than worrying about vectors of length bottom. The other side of that coin is that it makes perfect sense to have partial *computations* in types as long as they're somehow distinguished from total values, and as long as the system remembers not to *run* them until run-time. My point: it isn't all or nothing -- there's a slider here, and we can shift it a bit at a time. Conor, is Epigram currently under development? We've even stopped working on the engine and started working on the chassis. I'm in an intensive teaching block until the end of April, but from May it becomes Priority. The Reusability and Dependent Types project studentship will hopefully bring an extra pair of hands, come October. Epigram exists to be stolen from, so I'll be trying to encourage a literate programming style and plenty of blogging. We've spent a lot of time figuring out how to make the system much more open and modular, so it will hopefully prove easier for people to contribute to as well as to burgle. The worst thing about Epigram 1 was just how monolithic and impenetrable the code base became. It was a valuable learning experience but no basis for further progress. This time, we optimize for clarity. I don't see any conflict -- indeed I see considerable synergy -- in working simultaneously on the experimental frontier of dependent type systems and on the pragmatic delivery of their basic benefits via a much more established language like Haskell. Indeed, I think we'll learn more readily about the engineering realities of developing applications with dependent types by doing plenty of the latter. I don't think functional programmers should wait for the next generation of languages to mature before picking up this particular habit... All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Dan On 14 Mar 2009, at 14:26, Dan Doel wrote: On Saturday 14 March 2009 8:12:09 am Conor McBride wrote: Rome wasn't burnt in a day. Of course I want more than just numerical indexing (and I even have a plan) but numeric constraints are so useful and have so much of their own peculiar structure that they're worth studying in their own right, even for languages which do have full dependent types, let alone Haskell. We'll carry out this project with an eye to the future, to make sure it's compatible with full dependent types. One should note that ATS, which has recently been generating some excitement, doesn't have full dependent types, depending on what exactly you mean by that. I'm really impressed by the results ATS is getting, and by DML before it. I think these systems do a great job of showing what can be gained in performance by improving precision. For instance, it's dependent typing for integers consist of: I certainly want 1) A simply typed static/type-level integer type which looks exactly like the value-level integers and has a helpful but not exhaustive selection of the same operations. But this... 2) A family of singleton types int(n) parameterized by the static type. For instance, int(5) is the type that contains only the run-time value 5. 3) An existential around the above family for representing arbitrary integers. ...I like less. where, presumably, inspecting a value of the singleton family informs the type system in some way. But, we can already do this in GHC (I'll do naturals): -- datakind nat = Z | S nat data Z data S n -- family linking static and dynamic data NatFam :: * - * where Z :: NatFam Z S :: NatFam n - NatFam (S n) -- existential wrapper data Nat where N :: forall n. NatFam n - Nat Of course, ATS' are built-in, and faster, and the type-level programming is probably easier, but as far as dependent typing goes, GHC is already close (I don't think you'd ever see the above scheme in something like Agda or Coq with 'real' dependent types). Which is why I'd rather not have to do that in Haskell either. It really hurts to go through this rigmarole to make this weird version of Nat. I'd much rather figure out how to re-use the existing datatype Nat. Also, where the GADT coding really doesn't compete with ATS is in dealing with constraints on indices that go beyond unification -- numbers have more structure and deserve special attention. Numerical indexing systems need to carry a big stick for boring algebra if we're to gain the power but keep the weight down. But wherever possible, I'd prefer to avoid doing things an awkward way, just because we don't quite have dependent types. If the above kludge is really necessary, then it should at least be machine- generated behind the scenes from ordinary Nat. I'd much rather be able to lift a type to a kind than have a separate datakind feature. Apart from anything else, when you get around to indexed kinds, what you gonna index /them/ with? Long term, I'd far rather think about how to have some sort of dependent functions and tuples than muddle along with singletons and weak existentials. So this sort of type-level vs. value-level duplication with GADTs tying the two together seems to be what is always done in ATS. This may not be as sexy as taking the plunge all the way into dependent typing ala Agda and Coq, but it might be a practical point in the design space that GHC/Haskell- of-the- future could move toward without too much shaking up. And if ATS is any indication, it allows for very efficient code, to boot. :) I'd certainly agree that ATS demonstrates the benefits of moving in this direction, but I think we can go further than you suggest, avoiding dead ends in the design space, and still without too much shaking up. I don't think the duplicate-or-plunge dilemma you pose exhausts the options. At least, I seem no reason to presume so and I look forward to finding out! To be honest, I think the real challenge is to develop good libraries and methodologies for working with indexed types (and particularly, indexed notions of computation: what's the indexed mtl?). There are lots of promising ideas around, but it's hard to build something that scales whilst the encodings are so clunky. A bit of language design, even just to package existing functionality more cleanly, would really kick the door open. And yes, I am writing a research proposal. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
the nearly dependent near future, was Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Dan On 14 Mar 2009, at 18:48, Dan Doel wrote: On Saturday 14 March 2009 1:07:01 pm Conor McBride wrote: I don't think the duplicate-or-plunge dilemma you pose exhausts the options. At least, I seem no reason to presume so and I look forward to finding out! I didn't mean to suggest that ATS is the best you can do. Merely that you can still get a lot done without going very far beyond what is technically possible (though not enjoyable) in GHC today (to the point that people will actually categorize your language as dependently typed when it merely has a type language comparable in richness and convenience to the value level, but is still mostly separate). I'd certainly agree with that assessment. [..] If you can do better than ATS, and have value-level stuff automatically reproduced at the type level and suchlike, so much the better. I fully support that. :) Good! 'Cos that's what I'm going for. It certainly won't involve types depending on arbitrary expressions -- or even on run-time data in the first instance -- but by taking the approach of lifting what we can from types to kinds and from values to types, we keep those options open, as well as hiding the cruft. Note: subject about to slide into something a tad more technical, but I gotta tell you this one... To echo your remarks above, I'm pretty sure one could go quite far even with something as non-invasive as a GHC preprocessor. My opening gambit would be to extend the grammar of kinds as follows, with a translation (#) back to current kinds: kind ::= * #* = * | kind - kind #(j - k) = #j - #k | {type}#{t}= * | forall x :: kind. kind#(forall x :: j. k) = #k Note that this forall abstracts type-level stuff in a given kind, not kinds themselves, so the bound variable can only occur inside the {..} used to lift types up to kinds. Correspondingly, when we smash the {t} kinds all to *, we can dump the polymorphism. Now populate the {t} kinds by lifting expressions to the type level: these look like {e} where e :: t is built from fully applied constructors and variables. That's certainly a total fragment! The preprocessor will need to cook up the usual bunch of gratuitous type constructors, one for each data constructor used inside {..} in order to translate expressions to types. It will need to perform tighter checks on class and data declarations (ideally by constructing objects one level down which express an equivalent typing problem) but GHC already has the necessary functionality to check programs. It might be possible to cut down on the amount of {..} you need to festoon your code with. On the other hand, it might be good to delimit changes of level clearly, especially given existing namespace policies. It's not much but it's a start, it's super-cheap, and it's compatible with a much more sophisticated future. I program in this language already, then I comment out the kinds and types I want and insert their translations by hand. At the moment, I have to write types like data Case :: ({a} - *) - ({b} - *) - {Either a b} - * where InL :: f {a} - Case f g {Left a} InR :: g {b} - Case f g {Right b} rather than programs like, er... either. But perhaps we could also figure out how to translate either to a type function. However, the numeric constraints project will need more than a preprocessor, because it delivers specific new constraint-solving functionality during type inference, rather than just the precooking of first-order value unification problems as first-order type unification problems. Indeed, with rank-n types, it could be quite fun. I'm sure there are devils yet in details, but the prospects for not-quite-dependent types by re-use rather than hard labour look quite good, and forwards-compatible with yer actual dependent functions, etc, further down the line. We live in interesting times! All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pointless functors
On 13 Mar 2009, at 14:32, Ross Paterson wrote: On Fri, Mar 13, 2009 at 03:18:15PM +0100, Martijn van Steenbergen wrote: Are there any functors f for which no point/pure/return :: a - f a exists? No. Choose an arbitrary element shape :: f () and define point x = fmap (const x) shape Correspondingly, consider the functor Const Void. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Apologies for crossposting. Please forward this message to individuals or lists who may be interested. In addition to the recently advertised PhD position at Strathclyde on Reusability and Dependent Types, I am delighted to advertise the following PhD opportunity. {- -- Haskell Types with Numeric Constraints -} We are grateful to Microsoft Research for their sponsorship of this project, which includes an internship, and with it the chance to make a real difference to world of principled but practical programming. The project investigates the practical and theoretical impact of extending Haskell's type system with numeric expressions (representing sizes, or ranges, or costs, for example) and constraints capturing richer safety properties than are currently managed by static typing. It has three strands: (1) to investigate type inference with numeric constraints, (2) to investigate new programming structures, patterns, and techniques which exploit numeric indexing, and (3) to study the performance benefits derivable from richer guarantees. A bright student could bring significant benefits to developers using Haskell, a language with increasing industrial traction — not least at Microsoft. Work on the Glasgow Haskell Compiler, at Strathclyde! {-} The position is fully funded, covering stipend, fees (at the home/EU rate), equipment, and travel, starting in October 2009. The closing date for applications is 15th April 2009. For further details, see: http://personal.cis.strath.ac.uk/~conor/phds/ or email me (co...@cis.strath.ac.uk). I look forward to hearing from you. Yours c Conor McBride ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Microsoft PhD Scholarship at Strathclyde
Hi Bulat, hi all, On 10 Mar 2009, at 16:06, Bulat Ziganshin wrote: Hello Conor, Tuesday, March 10, 2009, 6:59:58 PM, you wrote: {- -- Haskell Types with Numeric Constraints -} are you have in mind integrating results into production ghc versions? Subject to rigorous quality control, community approval, and Official Permission, yes. We'll prototype first, of course, but the Microsoft sponsorship provides an ideal opportunity to work with GHC HQ on this. If we do a good job (so we need a good student) it should become part of the real deal. Only this morning, I was lecturing on combinators for 2-dimensional layout and apologizing for the need to manage the sizes for perfect fitting by smart constructor abstraction rather than typing. I really want to rectify that. I can imagine similar considerations affect hardware design libraries too, and goodness knows what else. Wire up numerical indexing to parametrized monads and not only are you cooking with gas, you might even know how much gas you're cooking with! So, yes. It's type-level integers that don't suck, and associated programming techniques, to be delivered via GHC and associated libraries. This is a real opportunity to make a difference (and also to stare out the window and watch the sun setting on central Glasgow, unless it's raining, which today it isn't). All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] question on types
Hi folks On 18 Feb 2009, at 10:35, Ryan Ingram wrote: On Wed, Feb 18, 2009 at 2:12 AM, Lennart Augustsson lenn...@augustsson.net wrote: Also, if you are using ghc you can turn on the extension that allows undecidable instances and make the type system Turing complete. snarkAnd you get the additional pain of a potentially nonterminating compiler without any of the nice type-level syntax that you really want when writing code at that level/snark Seriously, I love undecidable instances, but there's gotta be a way to make type-level programming less painful. GHC team: please give us type-level integers that don't suck! If I ever have to see S (S (S (S Z))) again it's too soon. Just to say that a formal advert will appear any day now, but I should strike while the iron is hot --- Microsoft Research have been generous enough to sponsor a PhD scholarship at the University of Strathclyde (supervised by me) on a project which, for reasons of public decorum is called Haskell Types with Numeric Constraints but which translates to type-level integers that don't suck and then some... Start date will be October 2009 or so. An internship at MSR is typically part of the package, and in this case is likely to involve experimenting with extensions to GHC. So, if you're ready, willing, and able to work on making Ryan's wishes come true, drop me a line to let me know you're interested in working on (dependent types for) Haskell in Glasgow. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Another point-free question (=, join, ap)
Hi Edsko On 13 Feb 2009, at 09:14, Edsko de Vries wrote: Hey, Thanks for all the suggestions. I was hoping that there was some uniform pattern that would extend to n arguments (rather than having to use liftM2, litM3, etc. or have different 'application' operators in between the different arguments); perhaps not. Oh well :) Will this do? http://www.haskell.org/haskellwiki/Idiom_brackets You get to write iI f a1 a2 a3 Ji for do x1 - a1 x2 - a2 x3 - a3 f a1 a2 a3 amongst other things... Cheers Conor This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Factoring into type classes
Hi folks I have been known to venture the viewpoint that the newtype trick might benefit from improved library support, for example, here http://www.mail-archive.com/haskell-cafe@haskell.org/msg37213.html This is in a similar vein to Derek's approach, if accompanied by a little more grotesque whizzbangery. On 19 Jan 2009, at 21:51, Derek Elkins wrote: On Mon, 2009-01-19 at 12:10 -0800, Iavor Diatchki wrote: Sure, the point is that you are essentially adding a type annotation, which is like using a non-overloaded function. Compare, for example: mappend add x y and getSum (mappend (Sum x) (Sum y)). I think that the first one is quite a bit more readable but, of course, this is somewhat subjective. data Iso a b = Iso { to :: a - b, from :: b - a } under :: Iso a b - (b - b) - (a - a) under iso = to iso ~ from iso under2 :: Iso a b - (b - b - b) - (a - a - a) under2 iso = to iso ~ under iso sumIso = Iso Sum getSum (+) = under2 sumIso mappend Perhaps it's worth trying to push in this direction, in search of a coherent kit. After all, there's a lot of structure out there. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Total Functional Programming in Haskell
Hi I've been reticent to join this thread as it has the potential to eat my life, but I thought I'd say some technical things. On 30 Sep 2008, at 22:54, Derek Elkins wrote: On Mon, 2008-09-29 at 20:02 -0700, Jason Dagit wrote: Maybe instead of using (-) as the function constructor for total functions we use a different symbol, say (|-), and the compiler knows to use the more specialized semantics on those definitions. I'm not sure how make this work for values that are total functional versus values that are just pure (partial) functional. This can be done exactly the same way it is done with IO. Remove general recursion* from Haskell and have a partiality monad with fix :: (a - a) - Partial a I'm not sure that's the best type for fix, to be honest (though it would do in a pinch). It doesn't nest very neatly. Some argue for sfix :: (a - Partial a) - Partial a which allows you to make partial computations from recursive values. Being a happy Haskeller, I'd prefer lfix :: (Partial a - Partial a) - Partial a which is probably just join . fix as you present it, but says that its body gets a computation which it can choose to run, or not, as appropriate. In the dependently typed world, remember there are two separate notions of operational semantics (1) the open evaluation used by the typechecker, reducing under lambda, etc (2) the closed evaluation used at run-time, with no computation under binders It should be straightforward to make lfix a constant in (1), whilst (2) would actually run it. So that is indeed very like IO, handing off computations to an unscrupulous run-time system. Of course, we'd provide laws to reason about Partial computations (monad laws, unrolling, fixpoint induction) with sufficient means to allow escape from Partial on presentation of a (non-Partial) termination proof (erased for (2)). That's all to say that we can set things up so you can pay as you go. Of course, that's just to say we can model the phenomena, not that we can present them ergonomically... But what of Haskell? This particular idea has been discussed several times in a couple of places. Most people seem to think it would be too much of a hassle to use. Not the most copper-bottomed of arguments, as well you know, but if programming in Partial entails clunky monadification of lovely terse applicative code, most people are probably right. However, what if we were to find a way to break that entailment? The idiom bracket notation is a step in that direction, but it's still not enough. Suppose we were to find a way to program with our usual notation, but with the extra freedom to vary the 'ambient' monad? We could choose Id for total programs, Partial for workaday slackness, and a whole bunch of other stuff at our convenience. We'd need some way to change the ambient monad locally, of course. To be frank, I don't know if such a setup could be made to fit with Haskell's existing design choices. But I think it's an attractive possibility, worth looking into. Locally, however, my point is to ask whether there's a specific hassle with the Partial monad beyond the usual notational annoyances that come with any monad. If so, that would be interesting to hear about, and new to my ears. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Compiler's bane
Hi On 29 Aug 2008, at 21:12, Jonathan Cast wrote: If you want to avoid infinite normal forms (or just plain lack of normal forms, as in let x = x in x or (\x - x x) (\ x - x x)), you need to follow three rules: 1) Static typing With you there. 2) No value recursion Mostly with you: might allow productive corecursion computing only on demand. 3) If you allow data types, no recursive data types I can think of a few Turing incomplete languages with (co)recursive data types, so Otherwise, your language will be Turing-complete, seems suspect to me. It's quite possible to identify a total fragment of Haskell, eg, by seeing which of your Haskell programs compile in Agda. Things aren't as hopeless as you suggest. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GLfloat on a Mac
Hi folks I thought I'd try a bit of OpenGL. Perhaps I should send this to the more specific list, but perhaps other people are, like me, trying out a variety of UI technology. I thought I'd give OpenGL a go, because I saw the name whizz by when I upgraded to 6.8.3. I found the tutorial and got copy-paste cracking. It was all going swimmingly while I did almost nothing, but then ghc started dying on me. I chopped down my failing code to this joyous specimen: HelloWorld.lhs contains -- module Main where import Graphics.Rendering.OpenGL import Graphics.UI.GLUT myFloat :: GLfloat myFloat = 0.0 main = return () -- $ ghc -package GLUT HelloWorld.lhs -o HelloWorld Illegal instruction I'm using ghc 6.8.3 on a Mac PowerBook G4. Googling OpenGL illegal instruction produced an unending choice of horror stories. What message am I not getting? Is there some crucial manual I'm not reading? Is there something which we should be being told on the relevant wiki page? Distressed Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GLfloat on a Mac
Hi Thanks for the quick response. On 12 Aug 2008, at 10:18, Brandon S. Allbery KF8NH wrote: On 2008 Aug 12, at 5:11, Conor McBride wrote: $ ghc -package GLUT HelloWorld.lhs -o HelloWorld Illegal instruction I'm using ghc 6.8.3 on a Mac PowerBook G4. Googling OpenGL illegal instruction produced an unending choice of horror stories. What message am I not getting? Is there some crucial manual I'm not reading? Is there something which we should be being told on the relevant wiki page? You need to find (or build) a G4-compatible ghc; the 6.8.3 build for Leopard (and Tiger?) was built for a G5, and the above is the result. This sounds like bad news to me. I wonder how broken this G5 ghc is for a G4. Perhaps it should be labelled G5 rather than PowerPC in the large print. I'm quite scared about trying to build ghc: I worry that it may involve confronting large areas of my ignorance. I'm running Mac OS X 10.4.11 on a 1.5GHz PowerPC G4 PowerBook with 768MB of memory. I've got gcc 4.0.0. I'm using the 6.8.3 build whose entry on this page http://www.haskell.org/ghc/download_ghc_683.html reads - MacOS X (PowerPC) * ghc-6.8.3-powerpc-apple-darwin.tar.bz2 This is a binary distribution for Mac OS X 10.4 (Tiger) on PowerPC G5 machines, prepared by Christian Maeder. It needs libreadline. 5.2.dylib and libncurses.5.dylib under /opt/local/lib/. libgmp.a is statically linked in. - Now I'm wondering how badly I've shot myself in the foot. Alarmed Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GLfloat on a Mac
On 12 Aug 2008, at 11:19, Jules Bean wrote: Conor McBride wrote: This sounds like bad news to me. I wonder how broken this G5 ghc is for a G4. Perhaps it should be labelled G5 rather than PowerPC in the large print. I'm quite scared about trying to build ghc: I worry that it may involve confronting large areas of my ignorance. I'm running Mac OS X 10.4.11 on a 1.5GHz PowerPC G4 PowerBook with 768MB of memory. I've got gcc 4.0.0. I'm using the 6.8.3 build whose entry on this page FWIW, I use ghc on my G4 and I got it by compiling from MacPorts. It took the best part of day, but the resulting binary works. I'm not sure whirl is the right word, but I'll give it one anyway. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GLfloat on a Mac
On 12 Aug 2008, at 11:27, Conor McBride wrote: On 12 Aug 2008, at 11:19, Jules Bean wrote: FWIW, I use ghc on my G4 and I got it by compiling from MacPorts. It took the best part of day, but the resulting binary works. I'm not sure whirl is the right word, but I'll give it one anyway. After a very long time, it fell over with a large error message that I don't understand. Somehow, I'll get over it. I can't help thinking that this stuff shouldn't be hard. And yet it is. Sorry to anyone for whom this is just spam, and much gratitude to clued in people who can tell me in which particular way I'm being an idiot at the moment. All the best Conor oops Description: Binary data ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Hi Statutory mathematics warning: lots. On 5 Jun 2008, at 15:40, Jonathan Cast wrote: On 5 Jun 2008, at 1:39 AM, Thomas Davie wrote: Even deriving an instance of Functor seems rather implausable, what should it do for data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b) Should fmap's function argument operate on 'a's, 'b's, or both? class Functor (f :: * - *) where ... so, 'b's. While application remains injective, that seems appropriate. But wouldn't we want more, eg, that Wierd is a bifunctor (and, moreover, bitraversable, bihalfzippable,...)? Of course, there's a whole ghastly family of these things for type constructors of varying arities, together with stuff like the fixpoint of a bifunctor is a functor. jcc PS Why isn't Functor derivable? It would be very handy, but it's the tip of the iceberg. Being an Ulsterman, I get nervous about engineering for machinery-iceberg collisions. Perhaps it's worth looking for a systematic approach to the more general situation (not necessarily kind polymorphism; a systematic library treatment of n-functors for n in {0,..,pickamax} would be a good start). An alterative, perhaps, is to replace arity by indexing. This may get hairy. Untested stuff... data Rewired f n where Nil :: Rewired f Zero A :: f Zero - Rewired f Zero - Rewired f Zero B :: f One - Rewired f Zero - Rewired f Zero data Pick a b n where -- clearly a bit specific PickA :: a - Pick a b Zero PickB :: b - Pick a b One type Wierd a b = Rewired (Pick a b) Zero Here Rewired :: (* - *) - (* - *), but (* - *) means *-indexed type not container. I'd rather be more precise and work with (i - *) - (o - *), but we have to take i = o = * for now. The idea is to transform a bunch of input datatypes indexed by i to a bunch of output datatypes indexed by o. In this example, we collect Bob's two element types into a single GADT which specializes differently at two distinct input indices. There's no variation in the output index, so I just made them all Zero. But here's another old friend data Vec f n where Nil :: Vec f Zero Cons :: f Zero - Vec f n - Vec f (Suc n) which has no input variation, but uses the output index to specify length. Anyhow, the point is that for these indexed structures, you get to define much of the generic kit once and for all, and you get one obvious notion of map. type f :-: g = forall x. f x - g x class IxMap c where ixMap :: (f :-: g) - (c f :-: c g) Painless! Well, er, probably not. (Masochists may choose to generalize this notion by relaxing the index-preservation requirement to some sort of index-simulation, thus heading for Hancock's notion of container driver. I digress.) Anyhow, it would be nice if kit developed once for indexed structures could be lifted automatically to the indexed encoding of the more specific types you'd actually like to work with. Maybe that's a thing to be deriving. {-- Exercises for masochists (especially myself): (1) Show that simply-typed lambda-terms have IxMap structure (aka type-safe renaming) over notions of typed variable, just as untyped (de Bruijn) lambda-terms are an instance of Functor. It may help to think systematically about notions of typed variable. (2) Define an indexed container transformer IxFix :: ((* - *) - (* - *)) - ((* - *) - (* - *)) in such a way that instance IxMap c = IxMap (IxFix c) and present Vec, etc, with IxFix as the only source of recursive datatype definition. Hint, the more refined kind should be seen as (((i + o) - *) - (o - *)) - ((i - *) - (o - *)) so that c has places both for i-indexed inputs and for o-indexed substructures. (3) Grok and adapt the rest of Jeremy Gibbons' origami apparatus. --} Meanwhile, if you want to derive filtering, think about what one-hole contexts for elements need to look like, especially if you might want to throw the element away. Fans of bifunctor fixpoints and multivariate partial differentiation may be amused to note that [x] = mu y. 1 + xy (d/dx) (1 + xy) = y and that Cetin's Tab x = mu y. 1 + xy + y^3 (d/dx) (1 + xy + y^3) = y so perhaps a pattern is emerging... It's been an interesting day: thanks to all for the food for thought. It's clear that Haskell (with recent extensions) can now express very powerful abstractions such as indexed container, but not in a way which sits very comfortably with normal usage. I think that's a serious concern. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Examples of using Haskell for mathematics
Hi On 28 May 2008, at 10:33, Jose A. Ortega Ruiz wrote: [..] I've enjoyed immensely several entries in Dan Piponi's 'A Neighborhood of Infinity'. In particular, 'Infinitesimal rotations and Lie algebras': http://sigfpe.blogspot.com/2008/04/infinitesimal-rotations-and- lie.html made me decide once and for all that i want to grok Haskell. It's this sort of positivity that prompted us to invite Dan to speak at MSFP 2008 in Iceland. His blog is full of such lovely connections between functional programming and mathematics: it is a source of much happiness and wonder. Shameless plug. http://msfp.org.uk/ Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] bottomless Top?
Folks [statutory warning: functors, terminal objects, unsafeCoerce] I had a peculiar notion this morning to wonder whether I could get away with shape :: Functor f = f a - f () shape fa = unsafeCoerce fa Sure enough, ghci gives me *Top shape moo [(),(),()] *Top shape [undefined] [*** Exception: Prelude.undefined which shows that pattern matching does just enough work to check that an element of () isn't bottom. I'm just wondering if that's really what's happening, what other implementations do, and how the garbage collector would react: would all those a's hang around for as long as the shape? I'm also wondering whether it makes sense to have a bottomless Top type, with constructor _ and lazy pattern _ (with (undefined :: Top) equal to _). Then the constant-time shape operator makes the same sort of sense as the constant-time inflate :: Functor f = f Zero - f a Any thoughts on either or both? Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] bottomless Top?
Replying slap-foreheadedly to own post... On 15 May 2008, at 11:56, Conor McBride wrote: Folks I'm also wondering whether it makes sense to have a bottomless Top type, with constructor _ and lazy pattern _ (with (undefined :: Top) equal to _). Then the constant-time shape operator makes the same sort of sense as the constant-time inflate :: Functor f = f Zero - f a We've got it already. data One would do, with smart constructor only :: One only = undefined and no other operations, so no way to be strict in its values. It's the lazy version of Zero. Assuming (safely?) that representation of data in each instance of a type constructor is uniform, that means shape :: Functor f = f a - f One shape = unsafeCoerce should be ok, right? The question about the GC implications of that move still stands, though. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] bottomless Top?
On 16 May 2008, at 01:13, Jonathan Cast wrote: On 15 May 2008, at 4:29 AM, Conor McBride wrote: Replying slap-foreheadedly to own post... On 15 May 2008, at 11:56, Conor McBride wrote: Folks I'm also wondering whether it makes sense to have a bottomless Top type, with constructor _ and lazy pattern _ (with (undefined :: Top) equal to _). Then the constant-time shape operator makes the same sort of sense as the constant-time inflate :: Functor f = f Zero - f a We've got it already. data One would do, with smart constructor only :: One only = undefined As I've mentioned before, my favorite data type newtype One = One One does the same, and stays in Haskell 98. That's rather fun. On the face of it, it looks peculiar that *Top case undefined of One _ - True True until you put your newtype constructor sunglasses on. Funny that newtype constructors really are like id until you fmap them. Or is that optimized away these days? (And has the same weakness to seq: (`seq` ()) is perfectly strict (it's const undefined)). Oh b! I'd forgotten that seq lets you look at an undefined thing just enough to go wrong. It'd be lovely to have proper unit and product, with their eta-laws, compiling pattern matching to projection. Was it so bad to distingush the value types at which seq could be applied? Meanwhile, the game's up for the unsafeCoerce dodge: *Top shape ['m', undefined, 'o'] [(),*** Exception: Prelude.undefined I knew it was too good to be true. Like Randy Pollack says, the best thing about working in strongly normalizing languages is not having to normalize things. Loose morals are neither fast nor correct. I'd better crawl back under my rock. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: (flawed?) benchmark : sort
Hi On 14 Mar 2008, at 21:39, Aaron Denney wrote: On 2008-03-14, Conor McBride [EMAIL PROTECTED] wrote: Hi On 13 Mar 2008, at 23:33, Aaron Denney wrote: On 2008-03-13, Conor McBride [EMAIL PROTECTED] wrote: For a suitable notion of = on quotients, and with a suitable abstraction barrier at least morally in place, is that really too much to ask? I really think it is. I don't think the case of equivalent for this purpose, but not that purpose can be ignored. Sure. But use the right tools for the job. So what are the right tools then? Why is a typeclass not the right tool? I guess I mean to distinguish *equality*, which is necessarily respected by all observations (for some notion of observation which it's important to pin down), from coarser equivalences where respect takes careful effort. Take Roman's example of alpha-equivalence for the lambda-terms with strings for bound variables. No way would I ever call that equality, because respecting alpha-equivalence takes quite a lot of care. (Correspondingly, I'd switch to a representation which admitted equality.) [..] Of course, if you want to expose the representation for some other legitimate purpose, then it wasn't equality you were interested in, so you should call it something else. I'm perfectly happy calling it Equivalence. I'm perfectly happy having equivalences around, but if Eq means has an equivalence rather than has equality, then I'm not very happy about the use of the == sign. [..] That's a workable definition, but I don't know if I'd call it a sort, precisely. The standard unix tool tsort (for topological sort, a bit of a misnomer) does this. Will that do? Unfortunately, one can't just reuse the standard algorithms. Indeed. (Does anyone know a topological sort algorithm which behaves like an ordinary sort if you do give it a total order? Or a reason why there's no such thing?) So you're probably right that x = y \/ y = x should hold for the order relation used by library sort. That's not the axiom I was thinking of dropping when I said sort's type was too tight (it was you who brought up incomparability): I was thinking of dropping antisymmetry. If a sort can't support the standard sort on this key technique, and don't munge everything for two keys that compare equal, something is wrong. And I don't think sort is that special a case. I quite agree. That's why I'm suggesting we drop antisymmetry as a requirement for sorting. Instances, rather than explicit functions, are nice because they let us use the type system to ensure that we never have incompatible functions used when combining two data structures, or pass in a function that's incompatible with the invariants already in a data structure built with another function. I'm not sure what you mean here. So we surely do need an equivalence relation typeclass. And there are Eq instances that aren't quite equality, but are equivalences, and work with almost all code that takes Eq instances. My main concern is that we should know where we stand. I think it would be a very good thing if we knew what the semantic notion of equality should be for each type. What notion of equality should we use in discussion? What do we mean when we write laws like map f . map g = map (f . g) ? I write = to distinguish it from whatever Bool-valued function at some type or other that we might call ==. Given sneaky ways to observe memory pointers or fairly ordinary ways to expose representations which are supposed to be abstract, it's clearly impossible to ensure that = is absolutely always respected. It would be good if it was clear which operations were peculiar in this way. I'd like to know when I can reason just by replacing equals for equals, and when more care is required (eg, when ensuring that substitution respects alpha- equivalence). From the point of view of reasoning (informally or formally) it then becomes useful to know that some binary Bool-valued function is sound with respect to = and complete when one argument is defined and finite. It's useful to know that one is testing equality, rather than just some equivalence, because equality supports stronger reasoning principles. Equivalences are useful too, but harder to work with. I quite agree that we should support them, and that it is reasonable to do so via typeclasses: if a type supports multiple useful equivalences, then the usual newtype trick is a reasonable enough way to manage it. The only time treating equalities as equivalences won't work is when we need to coalesce equivalent elements into one representative, and the choice of representative matters. Another time when treating equalities just as equivalences won't do is when it's time to think about whether your program works. This issue is not just an operational one, although in the case of TypeRep, for example, it can get pretty near the bone. So, do we mark equivalencies as special, or observational
Re: Some clarity please! (was Re: [Haskell-cafe] Re: (flawed?) benchmark : sort)
Hi On 14 Mar 2008, at 03:48, Roman Leshchinskiy wrote: Adrian Hey wrote: I would ask for any correct Eq instance something like the law: (x==y) = True implies x=y (and vice-versa) which implies f x = f y for all definable f which implies (f x == f y) = True (for expression types which are instances of Eq). This pretty much requires structural equality for concrete types. For abstract types you can do something different provided functions which can give different answers for two equal arguments are not exposed. How do you propose something like this to be specified in the language definition? The report doesn't (and shouldn't) know about abstract types. Why not? Why shouldn't there be at least a standard convention, if not an abstype-like feature for establishing an abstraction barrier, and hence determine the appropriate observational equality for an abstract type? So you can either require your law to hold everywhere, which IMO isn't a good idea, or you don't require it to hold. From the language definition point of view, I don't see any middle ground here. Why not demand it in the definition, but allow unsafe leaks in practice? As usual. Why are you so determined that there's nothing principled to do here? People like to say Haskell's easy to reason about. How much of a lie would you like that not to be? Also, when you talk about definable functions, do you include things like I/O? What if I want to store things (such as a Set) on a disk? If the same abstract value can have multiple representations, do I have to convert them all to some canonical representation before writing them to a file? Canonical representations are not necessary for observational congruence. Representation hiding is enough. This might be rather slow and is, IMO, quite unnecessary. From a more philosophical points of view, I'd say that the appropriate concept of equality depends a lot on the problem domain. It's certainly true that different predicates may respect different equivalence relations. The equivalence relation you call equality should be the finest of those, with finer representational distinctions abstracted away. What that buys you is a class of predicates which are guaranteed to respect equality without further ado... Personally, I quite strongly disagree with restricting Eq instances in the way you propose. I have never found much use for strict structural equality (as opposed to domain-specific equality which may or may not coincide with the structural one). ...which is how we use equality when we think. I certainly don't think strict structural equality should be compulsory. In fact, for Haskell's lazy data structures, you rather need lazy structural simulation if you want to explain why cycle x = cycle xx What would be so wrong with establishing a convention for saying, at each given type (1) this is the propositional equivalence which we expect functions on this type to respect (2) here is an interface which respects that equivalence (3) here are some unsafe functions which break that equivalence: use them at your own risk ? Why is it pragmatically necessary to make reasoning difficult? I'm sure that wise folk out there have wise answers to that question which they don't consider to be an embarrassment. When representation-hiding is bliss, 'tis folly to be wise. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Some clarity please! (was Re: [Haskell-cafe] Re: (flawed?) benchmark : sort)
Hi folks I'm late into this thread, so apologies if I'm being dim. On 13 Mar 2008, at 16:17, [EMAIL PROTECTED] wrote: Adrian Hey [EMAIL PROTECTED] wrote: I would ask for any correct Eq instance something like the law: (x==y) = True implies x=y (and vice-versa) I wish I knew what = meant here. Did somebody say? I don't think it's totally obvious what equational propositions should mean. Nor do I think it's desirable to consider only those propositions expressible in QuickCheck. If = is reflexive and distinguishes undefined from True, then x = y implies (x == y) = True will be tricky to satisfy for quite a lot of types. What about undefined == undefined or repeat 'x' == repeat 'x' ? For some suitable (slightly subtle) definition of finite, you might manage x finite and x = y implies (x == y) = True One rather intensional definition of x = y might be x and y have a common n-step reduct with respect to some suitable operational semantics. I don't think this is what Adrian had in mind, but it certainly falls foul of Wolfram's objection. The easiest counterexample are sets (or finite maps) provided as an abstract data type (i.e., exported without access to the implementation, in particular constructors). Different kinds of balanced trees typically do not produce the same representation for the same set constructed by different construction expressions. This suggests that we should seek to define x = y on a type by type basis, to mean x and y support the same observations, for some suitable notion of observation, which might depend crucially on what operations are exported from the (notional or actual) module which defines the type. If so, it's clearly crucial to allow some observations which rely on waiting for ever, in order to avoid _|_-induced collapse. Something of the sort should allow this... Therefore, (==) on sets will be expected to produce equality of sets, which will only be an equivalence on set representations. ...but this... which implies (f x == f y) = True (for expression types which are instances of Eq). This specifies that (==) is a congurence for f, and is in my opinion the right specification: (==) should be a congurence on all datatypes with respect to all purely defineable functions. ...is more troublesome. Take f = repeat. Define f = f. I'd hope x == y = True would give us x = y, and that x == y would be defined if at least one of x and y is finite. That implies f x = f y, which should guarantee that f x == f y is not False. But at least nowadays people occasionally do export functions that allow access to representation details, [..] I consider this as an argument to remove showTree from the interface of Data.Set, and to either specify toList to produce an ordered list (replacing toAscList), or to remove it from the interface as well. Perhaps that's a little extreme but I agree with the sentiment. How about designating such abstraction- breaking functions nosy, in the same way that functions which might break purity are unsafe. (mapMonotonic should of course be removed, too, or specified to fail (preferably in some MonadZero) if the precondition is violated, which should still be implementable in linear time.) What's wrong with mapMonotonic that isn't wrong with, say, sortBy?, or Eq instances for parametrized types? but if so would like to appeal to movers and shakers in the language definition to please decide exactly what the proper interpretation of standard Eq and Ord class laws are and in the next version of the report give an explanation of these Strongly seconded, inserting ``precise'' before ``explanation'' ;-) (And I'd expect equivalences and congruences to be accessible on the basis of standard first-year math...) Before we can talk about what == should return, can we settle what we mean by = ? I think we need to pragmatic about breaking the rules, given suitable documentation and maybe warnings. We should at least aspire to some principles, which means we should try to know what we're talking about and to know what we're doing, even if we don't always do what we're talking about. I'll shut up now. Potatoes to peel Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: (flawed?) benchmark : sort
Hi On 13 Mar 2008, at 22:28, [EMAIL PROTECTED] wrote: G'day all. Quoting Adrian Hey [EMAIL PROTECTED]: What's disputed is whether or not this law should hold: (a == b) = True implies a = b Apart from possibly your good self, I don't think this is disputed. Quotient types, as noted elsewhere in this thread, are very useful. For a suitable notion of = on quotients, and with a suitable abstraction barrier at least morally in place, is that really too much to ask? Their common use predates Miranda, so it's way too late to unbless them now. How depressing! Untyped programming also predates Miranda. We can always aspire for better. It's not that we need to get rid of Quotients: it's just that we need to manage information hiding properly, which is perhaps not such a tall order. Meanwhile, the sort/Ord/OrdWrap issue may be a storm in a different teacup: the type of sort is too tight. Ord (total ordering) is way too strong a requirement for sorting. Antisymmetry isn't needed for sorting and isn't possessed by OrdWrap. A bit more structure for order-related classes would surely help here. Isn't there room for hope? All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: (flawed?) benchmark : sort
Hi On 13 Mar 2008, at 23:33, Aaron Denney wrote: On 2008-03-13, Conor McBride [EMAIL PROTECTED] wrote: Hi On 13 Mar 2008, at 22:28, [EMAIL PROTECTED] wrote: G'day all. Quoting Adrian Hey [EMAIL PROTECTED]: What's disputed is whether or not this law should hold: (a == b) = True implies a = b Apart from possibly your good self, I don't think this is disputed. Quotient types, as noted elsewhere in this thread, are very useful. For a suitable notion of = on quotients, and with a suitable abstraction barrier at least morally in place, is that really too much to ask? I really think it is. I don't think the case of equivalent for this purpose, but not that purpose can be ignored. Sure. But use the right tools for the job. Now, it may be the case that fooBy functions are then the right thing, but it's not clear to me at all that this is true. And if the fooBy option works, then why would the foo option fail for equivalence classes? It seems reasonable to construct quotients from arbitrary equivalences: if fooBy works for the carrier, foo should work for the quotient. Of course, if you want to expose the representation for some other legitimate purpose, then it wasn't equality you were interested in, so you should call it something else. A bit more structure for order-related classes would surely help here. Say what? Don't panic! If I don't have a total ordering, then it's possible two elements are incomparable Quite so. -- what should a sort algorithm do in such a situation? Not care. Produce a resulting list where for any [..., x, ..., y, ...] in the result, y = x implies x = y. Vacuously satisfied in the case of incomparable elements. In the case of a total order, that gives you y = x implies x = y (and everything in between), but for a preorder, you put less in, you get less out. Will that do? Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe