Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
Alexander Solla wrote: And denotational semantics is not just nice. It is useful. It's the best way to understand why the program we just wrote doesn't terminate. Denotational semantics is unrealistic. It is a Platonic model of constructive computation. Alan Turing introduced the notion of an oracle to deal with what we are calling bottom. An oracle is a thing that (magically) knows what a bottom value denotes, without having to wait for an infinite number of steps. Does Haskell offer oracles? If not, we should abandon the use of distinct bottoms. The /defining/ feature of a bottom is that it doesn't have an interpretation. Huh? I don't see the problem. Introducing bottom as a value is a very practical way to assign a well-defined mathematical object to each expression that you can write down in Haskell. See http://en.wikibooks.org/wiki/Haskell/Denotational_semantics It's irrelevant whether _|_ is unrealistic, it's just a mathematical model anyway, and a very useful one at that. For instance, we can use it to reason about strictness, which gives us information about lazy evaluation and operational semantics. Best regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] State Machine Composition
Daniel Waterworth da.waterwo...@gmail.com wrote: I made this simple state machine combinator library today. I think it works as a simple example of a good use for GADTs. https://gist.github.com/1507107 Aren't your examples all special cases of the generic automaton arrow? There are two ways to represent it, both with their advantages and disadvantages: newtype Auto a b = Auto (a - (b, Auto a b)) countFrom :: Int - Auto a Int countFrom n = Auto (\_ - (n, countFrom (succ n))) or: data Auto a b = forall s. Auto s ((a, s) - (b, s)) countFrom :: Int - Auto a Int countFrom n0 = Auto n0 (\(_, s) - (s, succ s)) These state machines have local state and can be composed using applicative and arrow interfaces: liftA2 (+) (countFrom 3) (countFrom 5) proc x - do n1 - countFrom 10 - () n2 - someOtherMachine - x anotherMachine - n1 + n2 Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife = sex) http://ertes.de/ signature.asc Description: PGP signature ___ 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 Mon, Dec 19, 2011 at 8:20 PM, Robert Clausecker fuz...@gmail.com wrote: Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different? Thanks in advance for all answers, yours Robert Clausecker A whole lot (a surprisingly very large amount) of things don't require breaking compatibility. Also a lot of things are really amazing but need smarter people than myself to invent them (the Constraint kind is a good example). And many things are trivial and superficial. I agree with everyone who mentioned it about giving things user-friendly names and leaving the mathematical connections to the documentation. I'm partial to Mappable/Sequenceable/Runnable for Functor/Applicative/Monad, but doubtless better ones are possible. I would define Monad in terms of join :p, and use (=) as the default bind. I also agree with name: Type instead of name :: Type. I would make : bind tighter. I would rename the * kind to Type, because (Type - Constraint) looks less weird than (* - Constraint). I would change some things to be just a little bit more C/Unix-like: != for inequality, allow (not require!) opening and closing braces on the same line, * instead of _ as the wildcard. Many things are in the realm of this could definitely be done better, but I'm not sure how, either: tuples, records, and modules, in ascending order. Records would be lens-based because composability is nice, but that's about as far as I know. The operative principle with modules would be that after 'import Module' you should be good to go: manual intervention to avoid name clashes is a very nice feature, but you should only have to use it rarely. (In other words, much more control would be given to module authors over how things are exported.) Modules would be parametrizable on types - for example, for FRP libraries where every signature includes the Time type. (If I knew more about ML-style modules I might be advocating them.) I would make the whitespace around infix operators (and other punctuation like list literals) mandatory and significant. It's how you write it in most cases anyways, and how you should have in most of the rest. This frees up a lot of syntax space which could be used for various things: special built-in syntax, prefix/postfix operators, and you could have normal-looking array[and] record.access like every other language. (To be clear, list literals would still look [like, this], it's just the presence or absence of whitespace in between them and the preceding identifier which would be significant in this case.) Strictness types can be added as a language extension but either way I would add them. I would put greater emphasis on unboxed polymorphism by multiinstantiation over polymorphism by boxing and dictionary passing (it's not nice that abstract code is slower than monotyped code), but that's an implementation issue. I would add language support for mutating values without explicitly using an IORef, provided you're doing it in the right monad and the effects don't leak, like what Disciple has but with better syntax. I would distinguish things which read from memory in an impure way from things which write to memory from things which Do Things In The Outside World like write a file. (Maybe by lifting Disciple's effect typing wholesale, but I'm attached to monads.) ___ 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?
2011/12/22 Gábor Lehel illiss...@gmail.com On Mon, Dec 19, 2011 at 8:20 PM, Robert Clausecker fuz...@gmail.com wrote: Image you would create your own language with a paradigm similar to Haskell or have to chance to change Haskell without the need to keep any compatibility. What stuff would you add to your language, what stuff would you remove and what problems would you solve completely different? Thanks in advance for all answers, yours Robert Clausecker I would have compose (probably not called '.') read the same way we read this sentence (and unix pipes) ie left to right. I would not overload . to mean compose and module-access. Probably gadt could be the norm and classic 'data' could be removed. ___ 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?
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? ___ 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 Thu, Dec 22, 2011 at 4:19 AM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: Alexander Solla wrote: And denotational semantics is not just nice. It is useful. It's the best way to understand why the program we just wrote doesn't terminate. Denotational semantics is unrealistic. It is a Platonic model of constructive computation. Alan Turing introduced the notion of an oracle to deal with what we are calling bottom. An oracle is a thing that (magically) knows what a bottom value denotes, without having to wait for an infinite number of steps. Does Haskell offer oracles? If not, we should abandon the use of distinct bottoms. The /defining/ feature of a bottom is that it doesn't have an interpretation. Huh? I don't see the problem. Introducing bottom as a value is a very practical way to assign a well-defined mathematical object to each expression that you can write down in Haskell. See http://en.wikibooks.org/wiki/Haskell/Denotational_semantics It's irrelevant whether _|_ is unrealistic, it's just a mathematical model anyway, and a very useful one at that. For instance, we can use it to reason about strictness, which gives us information about lazy evaluation and operational semantics. As another example Not that long ago, Bob Harper was complaining on his blog about how you can't use induction to reason about Haskell functions. But, that's incorrect. What you can't use is induction based on a model where all data types are the expected inductively defined sets, and non-termination is modeled as an effect. This isn't surprising, of course, because Haskell's models (i.e. denotational semantics) aren't like that. But, once you know what Haskell's models are---they model types as domains, and data types are inductively defined _domains_, not sets---then you in fact get induction principles based on those models (see for instance, Fibrational Induction Rules for Initial Algebras). You need to prove two or three additional cases, but it works roughly the same as the plain ol' induction you seem to lose for having non-strict evaluation. And then you have one less excuse for not using a language with lazy evaluation. :) -- Dan * http://personal.cis.strath.ac.uk/~patricia/csl2010.pdf ___ 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?
Отправлено с 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. 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)? ___ 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?
I would have compose (probably not called '.') read the same way we read this sentence (and unix pipes) ie left to right. You can use from Control.Arrow for that if you want. Erik ___ 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] If you'd design a Haskell-like language, what would you do different?
On Fri, 2011-12-23 at 01:29 +0400, 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. IIRC in ML-derived languages there is difference between let and let rec. All implicit fix can be changed into explicit so I imagine that: let rec f x = x -- a - Partial a let g x = x -- a - a Regards signature.asc Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Riddle of the Buddhist Monk
On Wed, Dec 21, 2011 at 10:12 AM, Patrick Browne patrick.bro...@dit.iewrote: On 21/12/11, *Richard O'Keefe * o...@cs.otago.ac.nz wrote: So what exactly is the program supposed to do? I am trying to see whether Haskell modules can be used for blending[1]. The original MAUDE [2,3] program just sets up an arbitrary meeting point, which is assumed to be time-2 and location-2. Then in MONK_MEETS_HIMSELF the up and down versions of these are made match. To do this I wish to declare the function location in MONK_ON_MOVE. Then I require different equations for that same location function in MONK_ON_MOVE_DOWN and MONK_ON_MOVE_UP both of which import MONK_ON_MOVE. Finally, I wish to import MONK_ON_MOVE_DOWN and MONK_ON_MOVE_UP into MONK_MEETS_HIMSELF and use the combined set of equations to check locations. You can't do that in Haskell. All equations defining a function must occur contiguously in the same Haskell module. You've actually defined two separate functions, MONK_ON_MOVE_DOWN.location and MONK_ON_MOVE_UP.location. If you want to define a single function that blends their behaviors, you need to do that explicitly. For example, you might define these as partial functions, returning type Maybe LocationOnPath, and then try each implementation (in your case, 2 tries), until one of them returns a non-Nothing result. You could use type classes with overlapping instances to try to merge two different definitions of location, but it wouldn't work the way you want. The compiler would statically choose one implementation of location that would be used for a given type, rather than trying equations from both (as you desire, and as would happen in Maude). So far I cannot figure out how the location function and the constructors can be shared in this way using Haskell modules. I have tried various combination import/export options, type classes, and newtype. I have also tried to use Strings instead of constructors. I had trouble using Haskell equations with pure constructors. Due to my ignorance of Haskell semantics I am not sure what Constructor1 = Constructor2 means. But in the original Maude there are constructor only equations such as Timed2 = Timeu2 which in Maude means that the constructor Timed2 could be replaced with Timeu2. I wrote Haskell functions to try to achieve a similar effect e.g. timed2 :: TimeOfDay - TimeOfDay timed2 Timed2 = Timeu2 I'm not sure why top-level equations like Timed2 = Timeu2 (or even Just () = Nothing) aren't an error in GHC (or even a -Wall warning), but, as you've observed, this won't cause Timed2 to rewrite to Timeu2. Constructors in Haskell truly are constructors, they don't rewrite to something else (similar to the intention of the [ctor] annotation in Maude). To make it work, you'd have to manually separate out which of your terms are truly constructors and which ones are functions. Then write equations defining the functions. Be sure that all equations for a given function are in a given place. You could of course implement a rewrite system on top of Haskell, and the syntax probably wouldn't be that bad (someone's probably already done it). But you can't directly write Maude-style rewrite systems in Haskell; the two languages just work differently. [1] http://cseweb.ucsd.edu/~goguen/pps/taspm.pdf [2] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000456.html [3] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000462.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
