[Haskell] Strathclyde PhD Position
Applications are welcome from ANYWHERE for a Microsoft Research sponsored PhD position in the Mathematically Structured Programming group at the University of Strathclyde. Project: Real World Data with Dependent Types: Integrity and Interoperation Strathclyde supervisor: Dr Conor McBride Microsoft supervisor: Dr Don Syme Starting: October 2015 Tuition fees: fully funded or substantially subsidised, depending on residency status Stipend: £14,057K Contact: Conor, by 8 May 2015 Project Summary Data integrity, manipulation and analysis are key concerns in modern software, for developers and users alike. We are often obliged to work with a corpus of files – spreadsheets, databases, scripts – which represent and act on aspects of data in some domain. This project seeks to improve the integrity and efficiency with which we can operate in such a setting by * delivering a language for data models which expresses their conceptual structure, capturing what kinds of things exist in a given context, what data we expect to have about them, and when those data are consistent; * delivering a language for data views relative to a model, characterizing the expected content of a particular spreadsheet or database, whether considered a data source or an output; * exploiting the descriptions of models and views to support a richer tool chain for data editing, auditing, integration and analysis, whether by internal spreadsheet calculation or database query, or by interfacing with programming languages; * exploring the art of the possible in automating the discovery of views and models from extant data. Dependent type systems provide a uniform formalism for the contextualisation of data and the characterization of its consistency. They use types both as a data representation language and as a logic, and they do so in a manner amenable to mechanical checking. However, the prescriptive dependent type systems of Coq, Agda or Idris are not yet attuned to the open enumerations and extensible record types that we need to build up models of a data domain in a compositional, descriptive way. This project thus offers a broad spectrum of activity, encompassing theoretical innovation, language design, and tool development in support of existing applications and programming languages, notably Excel and F#. Small Print * More detail about the problem and the approach envisaged can be found in this blogpost https://pigworker.wordpress.com/2015/04/09/model-the-world-view-your-data-control-their-chaos/ and in these slides https://personal.cis.strath.ac.uk/conor.mcbride/dependent-up.pdf * Our hope is that the student will seek to undertake a paid internship at Microsoft Research, Cambridge, at some point during the PhD. * We are based here: https://www.google.co.uk/maps/place/Torre+Livingstone,+University+of+Strathclyde,+16+Richmond+St,+Glasgow+G1+1XQ/@55.8611055,-4.2435337,17z/ That's in the centre of Glasgow, Scotland, an amazing place. * We actively seek to promote diversity in our workplace. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
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: Holes in GHC
Hi
Sorry to pile in late...
On 13 Feb 2012, at 09:09, Thijs Alkemade wrote:
On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh andres.l...@googlemail.com
wrote:
Hi Thijs.
Sorry if this has been discussed before.
In my opinion, the main advantage of Agda goals is not that the type
of the hole itself is shown, but that you get information about all
the locally defined identifiers and their types in the context of the
hole.
[..]
Thanks for your feedback. Showing everything in scope that matches or
can match the type of a hole is certainly something I am interested
in, but I'm afraid it's out of the scope of this project.
That's not quite what Andres said, although it would also be a useful
piece of functionality.
If I might plug a bit of kit I knocked together recently, if you
cabal install shplit
(see also https://personal.cis.strath.ac.uk/~conor/pub/shplit/ )
you'll get the beginnings of an editor-assistant which just works as
a stdin-stdout transducer. I've been able to wire it into emacs quite
neatly and gedit more clunkily. I'm told vi should be no problem.
Shplit turns
foo :: [x] - [x]
foo xs{-?-} =
into
foo :: [x] - [x]
foo [] =
foo (x : xs) =
by (i) snarfing the datatype declarations from your file (no import
chasing yet) and adding them to a standard collection, (ii) figuring
out the type of the pattern variables given the type signature
provided. Shplit is still very dumb and makes no use of ghc's
typechecker: shplit's typechecker could be used just as easily to
mark up pattern variables with their types, as to do case analysis.
It is rather tempting to push further and make the thing label holes
with their types. Sometimes, the adoption of primitive technology is
a spur to design. If one adopts the transducer model, the question
then arises in what format might we insert this data into the file?.
In the case of typed holes, we can go with types in comments, or
(with careful use of ScopedTypeVariables) we can really attach them
in a way that would get checked.
I think it could be quite a lot of fun to build a helpful tool,
splitting cases, supplying type information, perhaps even offering
a menu of possible ways to build a term. I think the transducer
method is a relatively cheap (* major caveat ahead) and editor-neutral
way to go about it. If you fix a text format for the markup (i.e., for
requests to and responses from the transducer-collaborator), at worst
it's usable just by running the thing on the buffer, but with more
programmable editors, you can easily make more convenient triggers
for the requests, and you can parse the responses (e.g. generating
tooltips or lifting out a list of options as a contextual menu). The
adoption of the transducer model effectively separates the choice of
information and functionality from the design of the user interface,
which has certainly helped me to get on and do something.
The caveat is that transducers require not just parsing source code
but the ability to reconstruct it, slightly modified. Currently,
she and shplit have very selective, primitive technology for doing
this. Parsing-for-transduction is surely worth a proper think.
All the best
Conor
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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: ANNOUNCE: GHC 7.4.1 Release Candidate 1
Hi On 21 Dec 2011, at 22:41, Johan Tibell wrote: Built a bunch of packages using the 64-bit compiler on OS X Lion. Works fine. I'm a bit of a numpty when it comes to this sort of thing. I tried to install this version ghc-7.4.0.20111219-i386-apple-darwin.tar.bz2 under Leopard, and got this far bash-3.2$ sudo ./configure Password: checking for path to top of build tree... dyld: unknown required load command 0x8022 configure: error: cannot determine current directory I don't really know what this means. I'm kind of expecting that I have *no chance* of getting this to work on Leopard and should pop out for some other big cat. Is it worth trying harder just now, or should I lose the spots? Cheers Conor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC 7.4.1 Release Candidate 1
On 22 Dec 2011, at 16:08, Sean Leather wrote: I've built it from source (ghc-7.4.0.20111219-src.tar.bz2) on Leopard. I'd be happy to contribute my build if somebody tells me what to do. I hope somebody who knows does just that. Meanwhile, that sounds good to try for myself. My flat's a bit on the chilly side... Cheers Conor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ANNOUNCE: GHC 7.4.1 Release Candidate 1
On 22 Dec 2011, at 16:08, Sean Leather wrote: I've built it from source (ghc-7.4.0.20111219-src.tar.bz2) on Leopard. I'd be happy to contribute my build if somebody tells me what to do. I had a crack at this and got quite warm, literally and metaphorically. But, no, I didn't quite get there. And yes, it's some sort of libraries issue. Here's the barf... make -r --no-print-directory -f ghc.mk phase=final all inplace/bin/ghc-stage1 -fPIC -dynamic -H32m -O-package-name integer-gmp-0.4.0.0 -hide-all-packages -i -ilibraries/integer-gmp/. - ilibraries/integer-gmp/dist-install/build -ilibraries/integer-gmp/dist- install/build/autogen -Ilibraries/integer-gmp/dist-install/build - Ilibraries/integer-gmp/dist-install/build/autogen -Ilibraries/integer- gmp/.-optP-include -optPlibraries/integer-gmp/dist-install/build/ autogen/cabal_macros.h -package ghc-prim-0.2.0.0 -package-name integer-gmp -XHaskell98 -XCPP -XMagicHash -XUnboxedTuples - XNoImplicitPrelude -XForeignFunctionInterface -XUnliftedFFITypes -O2 - no-user-package-conf -rtsopts -odir libraries/integer-gmp/dist- install/build -hidir libraries/integer-gmp/dist-install/build -stubdir libraries/integer-gmp/dist-install/build -hisuf dyn_hi -osuf dyn_o - hcsuf dyn_hc libraries/integer-gmp/dist-install/build/GHC/ Integer.dyn_o libraries/integer-gmp/dist-install/build/GHC/Integer/GMP/ Internals.dyn_o libraries/integer-gmp/dist-install/build/GHC/Integer/ GMP/Prim.dyn_o libraries/integer-gmp/dist-install/build/GHC/Integer/ Logarithms.dyn_o libraries/integer-gmp/dist-install/build/GHC/Integer/ Logarithms/Internals.dyn_o libraries/integer-gmp/dist-install/build/ GHC/Integer/Type.dyn_o libraries/integer-gmp/dist-install/build/cbits/ gmp-wrappers.dyn_o libraries/integer-gmp/dist-install/build/cbits/ cbits.dyn_o libraries/integer-gmp/gmp/objs/*.o -shared -dynamic - dynload deploy -dylib-install-name /usr/local/lib/ghc-7.4.0.20111219/ `basename libraries/integer-gmp/dist-install/build/libHSinteger- gmp-0.4.0.0-ghc7.4.0.20111219.dylib | sed 's/^libHS//;s/[-]ghc.*//'`/ `basename libraries/integer-gmp/dist-install/build/libHSinteger- gmp-0.4.0.0-ghc7.4.0.20111219.dylib` -no-auto-link-packages -o libraries/integer-gmp/dist-install/build/libHSinteger-gmp-0.4.0.0- ghc7.4.0.20111219.dylib ld: duplicate symbol ___gmpz_abs in libraries/integer-gmp/gmp/objs/ add.o and libraries/integer-gmp/gmp/objs/abs.o collect2: ld returned 1 exit status make[1]: *** [libraries/integer-gmp/dist-install/build/libHSinteger- gmp-0.4.0.0-ghc7.4.0.20111219.dylib] Error 1 make: *** [all] Error 2 ...which makes me wonder just what I need to delete. This sort of issue is beyond my ken, but I'm willing to learn. I also have no especial attachment to Leopard. Clues appreciated Conor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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
Re: Superclass defaults
Hi On 2 Sep 2011, at 10:55, Jonas Almström Duregård wrote: On 31 August 2011 12:22, Conor McBride co...@strictlypositive.org wrote: I become perplexed very easily. I think we should warn whenever silent pre-emption (rather than explicit) hiding is used to suppress a default instance, because it is bad --- it makes the meaning of an instance declaration rather more context dependent. Perhaps a design principle should be that to understand an instance declaration, you need only know (in addition) the tower of class declaration s above it: it is subtle and worrying to make the meaning of one instance declaration depend on the presence or absence of others. Those are all good arguments, and you've convinced me that always warning is better. The question then comes down to whether that warning should ever be strengthened to an error. First of all, I think the design goal is quite clear: a class C can be re-factored into a class C with a superclass S, without disturbing any clients. Requiring client C to opt-out from the default implementation of S is a clear violation of the design goal. So I disagree that option 1 can be compatible with the design goal, but like you say the design goal might be at fault. Design goal 1 does not explicitly distinguish the scenarios where S is pre-existing or being introduced afresh. If the former, it's inaccurate to describe what's happening as refactoring C, for S is experiencing some fall-out, too. We should clearly seek more precision, one way or another. Also, if I understand you correctly, you say the current situation is exceptional, and suggest option 2 as a temporary solution to it. You seem convinced that these kind of situations will not appear in the future, but I'm not as optimistic about that. Even when superclass defaults are implemented, people will occasionally implement classes without realizing that there is a suitable intrinsic superclass (or add the superclass but not the default instance). People will start using the new class and give separate instances for the superclass, and eventually someone will point out that the there should be a default instance for the superclass. Now if option 1 is implemented, the library maintainers will be reluctant to add the superclass instance because it will break a lot of client code. I agree that such a scenario is possible. The present situation gives no choice but to do things badly, but things often get done badly the first time around anyway. Perhaps I'm just grumpy, but I think we should aim to make bad practice erroneous where practicable. Once the mistake is no longer forced upon us, it becomes a mistake that deserves its penalty in labour. Silent pre-emption is bad practice and code which relies on it should be fixed: it's not good to misconstrue an instance declaration because you don't know which instance declarations are somewhere else. Nonmonotonic reasoning is always a bit scary. From a library design perspective, we should certainly try to get these hierarchical choices right when we add classes. I accept that it should be cheap to fix mistakes (especially when the mistake is lack of foresight. Sticking with the warning rather than the error reduces the price of this particular legacy fix at the cost of tolerating misleading code. I agree that the balance of this trade-off is with the warning, for the moment, but I expect it to shift over time towards the error. But if it's clear what the issue is, then we can at least keep it under review. Will there be a solution to this dilemma that I have missed? Should the client code be allowed opt-out from the superclass preemptively before it is given a default? Won't that cause a similar perplexity? I don't know what you mean by this. Perhaps you could expand on it? All the best Conor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass defaults
Hi On 2 Sep 2011, at 16:34, Brandon Allbery wrote: I hope I am misunderstanding this I wrote: I agree that such a scenario is possible. The present situation gives no choice but to do things badly, but things often get done badly the first time around anyway. Perhaps I'm just grumpy, but I think we should aim to make bad practice erroneous where practicable. Once the mistake is no longer forced upon us, it becomes a mistake that deserves its penalty in labour. Silent pre-emption is bad practice and with the response: So, when the whole point is that an unfortunate design years ago can't be reasonably fixed without rewriting massive amounts of code, the only correct answer is to rewrite massive amounts of code? I'm not sure what you're asking here. Of course we should compare the pain of the treatment with that of the symptoms. Especially when the original proposal was put forward *specifically to avoid* rewriting massive amounts of code? Which original proposal? How does it avoid rewriting code? Yes, we'd love a perfect world. We don't have one. That's the *point*. Recall that Option 2 resolves the duplicate superclass instances in favour of an explicit prior instance, but issues a warning (which should offer the data to choose between explicit resolutions). That deals with a chunk of the legacy scenario (although it doesn't handle the situation where some M is made a Monad in one module and made Applicative in a later module, which is possible (common, even?) because Applicative is not currently a superclass of Monad). If we make one existing class a superclass of another existing class, some disruption is inevitable: we can try to minimize that disruption, but we can't eliminate it entirely. For another example, if some F is made Applicative and Traversable in the same module, which default Functor instance pre-empts the other? We should question whether the disruption of even Option 2/3 makes it worth adding default superclass instances at all. Maybe, depressingly, we've reached the can't-fix-it stage. It would be good to get some data. It's also worth considering tools to support migration, using the diagnostics generated by warnings. If it is worth adding default superclass instances, Option 2 looks like a crucial disruption-minimizing expedience, while we have a legacy of newly extraneous instances to deal with. As far as an unfortunate design years ago is concerned, we should be careful to minimize the amount of rewriting required. If that minimum is still too much, we'd better not go there. I'm in favour of moving to Option 1 eventually, as somehow the better choice for code comprehension. But I can see reasons to resist the changeover: * too much unmigrated code still relying on pre-emption under Option 2; * new instances of the old problem (an existing S is suddenly made a superclass of an existing C, with a default S instance for C) come into being, The former is a real risk, but hopefully with a finite lifespan. It would be too costly to switch from a warning to an error while too much code relies on the deprecated practice. Please don't imagine I'm in favour of that. The latter, however, requires us to be a bit dim in a way which was certainly not in evidence when most of the current motivating examples arose. In the legacy code (Monad-Applicative-Functor, Traversable-Foldable-Functor), we've had to choose between two bad options, but the candidate superclass-with-default-implementation has usually been evident. I'm sure we're capable of being that dim. I'm also sure we're capable of screwing up by writing an instance and assuming we get the default superclass instance we expect, without noticing that someone else's chunk of the codebase pre-empts it. I'd be troubled if someone knackered my applicative- style use of Monad [] by adding a zipping Applicative [], or even an instance which appeared to have the same functionality but also did some sneaky unsafePerformIO badness. That's an example of the risk we take by allowing pre-emption. We have to balance the risk of going back and resolving duplicates with the risk of bugs caused by code meaning less than it says. So, are default superclass instances just too disruptive? All the best Conor PS We'd love a perfect world. We don't have one. That's why we change things. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass defaults
On 2 Sep 2011, at 18:19, Jonas Almström Duregård wrote: I agree. Option 2 FTW :) The recent discussion concerns whether option 2 should eventually be shifted to option 1. Everyone seems to agree that option 2 should be used initially. A similar warning should perhaps indicate that a hiding clause has nothing to hide, as Jonas suggests. I'm in favour of Option 2 now and Option 1 later, where later has non-disruptiveness criteria attached. A bit like being in favour of the pound now and the euro later. As I've mentioned in another message just now, even Option 2 entails some disruption, when you make one old class a new superclass-with- default of another (e.g. Functor for Monad): if old code makes M a Functor in a later module than its Monad instance, that Functor M instance comes too late to pre-empt the default and is rejected as a duplicate. All the best Conor Regards, Jonas On 2 September 2011 18:55, Simon Peyton-Jones simo...@microsoft.com wrote: Too many words! I'm losing track. What I'm proposing is Option 2 under The design of the opt-out mechanism on http://hackage.haskell.org/trac/ghc/wiki/DefaultSuperclassInstances I believe that meets everyone's goals: * A warning encourages you to fix the client code * But you can turn it off, and it's not fatal. Does anyone advocate something else? Simon | -Original Message- | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users- | boun...@haskell.org] On Behalf Of Jonas Almström Duregård | Sent: 02 September 2011 16:50 | To: Conor McBride | Cc: GHC users | Subject: Re: Superclass defaults | | The question then comes down to whether that warning should ever be | strengthened to an error. | | Indeed. | | I agree that such a scenario is possible. The present situation gives | no choice but to do things badly, but things often get done badly the | first time around anyway. Perhaps I'm just grumpy, but I think we | should aim to make bad practice erroneous where practicable. Once | the mistake is no longer forced upon us, it becomes a mistake that | deserves its penalty in labour. Silent pre-emption is bad practice and | code which relies on it should be fixed: it's not good to misconstrue | an instance declaration because you don't know which instance | declarations are somewhere else. Nonmonotonic reasoning is always a | bit scary. | | From a library design perspective, we should certainly try to get these | hierarchical choices right when we add classes. I accept that it should | be cheap to fix mistakes (especially when the mistake is lack of | foresight. Sticking with the warning rather than the error reduces the | price of this particular legacy fix at the cost of tolerating misleading | code. I agree that the balance of this trade-off is with the warning, | for the moment, but I expect it to shift over time towards the error. | But if it's clear what the issue is, then we can at least keep it under | review. | | I agree. Making bad practice erroneous is good, but its not really the | bad practice that raises the error here. You have no serious problems | until you try to change your bad design to a good one. Like you say it | should be cheap to fix mistakes. | | Will there be a solution to this dilemma that I have missed? Should | the client code be allowed opt-out from the superclass preemptively | before it is given a default? Won't that cause a similar perplexity? | | I don't know what you mean by this. Perhaps you could expand on it? | | What I'm trying to ask is if you can write compatible code that will | work across gradual changes of the compiler and the libraries. | | Suppose we have library with class C. In a newer version of the | library we add an intrinsic superclass S. Also suppose the compiler | implements option 1. Now the users of the library want to write code | that uses both C and S, and that's compatible with both the new and | the old library. From what I can tell there are three situations that | needs to be covered: | | 1) Old compiler - Old library | Here we need to specify both instances, and we cant hide the default S | instance because its not supported by the compiler. This also applies | for other situations where the client must use Haskell 2010 compatible | code. | | 2) New compiler - Old library | Here we also need to specify both instances. | | 3) New compiler - New library | We can either write both instances and hide the default or we can just | write an instance for C. | | Clearly code that covers situation 1 will never be compatible with situation 3. | | The question I was asking was if we are allowed to hide the default | instance of S in situation 2. In that case you can write compatible | code for situation 2 and 3. The possible confusion from this is that | you hide a default implementation thats not defined. Maybe it's not as | bad as overriding
Re: Superclass defaults
Hi Sorry to be late again...I'm trying to have what's laughably described as a holiday, but it seems more like the common cold to me. On 31 Aug 2011, at 08:52, Jonas Almström Duregård wrote: | There seems to be a lot of support for Option 3... but what about Option 2 (ie pre-empt but give a warning)? At least in the short term, I think Option 2 is a good compromise. It's true that when I started using default superclass instances (which SHE supports) in the Epigram codebase, the first thing I had to do was delete a bunch of dull default instance stacks. That was fun, but it wasn't nothing. I think option 2 sounds very good. Possibly with the exception of only warning when the manual instance is in another module, since you will never experience the perplexity described in option 3 if you have written the instance yourself. I become perplexed very easily. I think we should warn whenever silent pre-emption (rather than explicit) hiding is used to suppress a default instance, because it is bad --- it makes the meaning of an instance declaration rather more context dependent. Perhaps a design principle should be that to understand an instance declaration, you need only know (in addition) the tower of class declaration s above it: it is subtle and worrying to make the meaning of one instance declaration depend on the presence or absence of others. Arguably, option 1 does not conflict with design goal 1. Design goal 1 supports a methodology for refining a class into a hierarchy without creating the need for stacks of default instances or breaking code. If the new superclass is a brand new thing without legacy instances, there's no problem. If we'd had this mechanism in place, Functor would always have been made a superclass of Monad, Applicative would have been easily inserted, and we wouldn't have the stacks of manually added default instances to worry about. The main problem with Option 1 is in dealing with the legacy of classes which currently require a stack of default instances, creating a hierarchy from parts which already exist. Option 1 would create a bunch of instance conflicts and thus demand changes to code. Design goal 1 isn't very explicit (sorry!) about this distinction between introducing new classes as superclasses and building hierarchies from legacy classes, but it was the former I intended. I always expected the latter to cause trouble. If it is also a design goal to minimize damage with respect to the current unfortunate situation, then Option 1 is problematic. Whatever we might wish, we are where we are. We should be pragmatic. I think we should set Option 1 as the direction of travel, but go with Option 2 for the moment. We should make sure that the warnings generated by Option 2 are sufficiently informative that it is easy to track down the conflicts and resolve them explicitly, for Option 1 compliance. Does this sound plausible? Conor ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass defaults
[resend to GHC users, now I've subscribed!] Hi Simon On 15 Aug 2011, at 11:36, Simon Peyton-Jones wrote: | Nice. But will it be happening soon, or not? And how soon is | soon? Not soon enough to be useful for this mappend question. But, concerning proposed extensions to GHC about class aliases/ superclass defaults etc, the truth is that the biggest reason for inertia here at GHC HQ is not so much the implementation effort (athough that is always an issue). Rather, it's uncertainty about (a) Is there a reasonably large group of users who really want such a change? Or is it just nice to have? (b) What is the right design? (c) Does it pay its way? (ie do the programming benefits justify the cost in terms of both language complexity and ongoing maintenance burden of one more feature to bear in mind when changing anything) If you care about the issue, maybe you can help resolve the above questions. In particular, to give concrete evidence for (b), working out some case studies would be a Good Thing. The examples given in other proposals using the extension proposed here would be one starting point. I can't speak for typical users, but I can relay my own experience. I added this feature to SHE last time there was an outbreak of Functor/Applicative/Monad, just to focus a bit of concrete thought on the matter. Hacking on Epigram the other day, I finally got annoyed enough (with dumb extra instances) to use it, so I wired in default superclass instances Functor for Applicative, Applicative for Monad Functor for Traversable, Foldable for Traversable Alternative for MonadPlus and then went on the rampage! Nothing broke. I got rid of a lot of cruft. I did make essential use of hiding instance Functor for structures which were both Applicative and Traversable. I cut tens of lines for the cost of one or two hidings. If someone felt able to act as moderator for the discussion, willing to summarise conclusions, open questions, and so on, on the wiki page, that would be enormously helpful. I'm up for that role, if that's appropriate. I am in too many inner loops. But I *am* willing to contemplate such an extension -- it has the same flavour as default methods themselves, which are a very useful part of H98. One thing that's really noticeable and sad about the status quo is that we can't refine the structure of a bunch of related classes without breaking established interfaces. I guess an interesting question might be what progress is effectively being blocked by our current inability to engineer around this problem. What are we stuck with just now? This is a recurring issue, at least as far as mailing list heat is concerned, but it would be good to have more evidence of substantial impact. The Monoid vs Semigroup issue is a case in point, perhaps. Folks, what do you think? Cheers Conor PS Are there any other default superclass instances for standard classes that SHE could usefully bake in? Sadly, we can't purge redundant methods from standard classes just yet, but we can at least get rid of boilerplate instances. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell] 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 mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[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] 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 mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[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: Functor hierarchy proposal and class system extension proposal
Hi On 2 Jan 2011, at 09:29, Malcolm Wallace wrote: See also http://repetae.net/recent/out/classalias.html http://www.haskell.org//pipermail/libraries/2005-March/003494.html http://www.haskell.org//pipermail/haskell-prime/2006-April/001344.html http://www.haskell.org//pipermail/haskell-prime/2006-August/001582.html A proposal from Jón Fairbairn for how to add default superclass method definitions gained some traction, and deserves to be revi(v/s)ed now, I think. Some superclass relationships are `shallow' interface extensions: MonadPlus does not give you a standard way to implement Monad, just more functionality within a monad. Other superclass relationships `deepen' existing functionality---if you have Ord, you can certainly make Eq; if you have Monad, you can certainly make Applicative, etc. The former is currently well supported, the latter badly. Jón's proposal was to improve the latter situation by allowing the subclass to specify a default (partial) implementation of a superclass. So we might write class Applicative f where return :: x - f x (*) :: f (s - t) - f s - f t instance Functor f where fmap = pure . (*) giving not only a subclass constraint (Functor f =) but also a standard means to satisfy it. Whenever an Applicative instance is declared, its Functor sub-instance is unpacked: buy one, get one free. This, on its own, is not quite enough. For one thing, we need a way to switch it off. I should certainly be permitted to write something like instance Applicative Blah where return = ... (*) = ... hiding instance Functor Blah to prevent the automatic generation of the superclass instance. The subclass constraint would still apply, so in order to use the Applciative functionality of Blah, it would have to be a Functor otherwise, e.g., by being Traversable. This `hiding' option was missing from Jón's proposal, but it seems crucial to address the potential for conflicts which was identified in the discussion at the time. It's also clear that we must be able to override the default behaviour. When the class declaration has a superclass instance, but not otherwise, a subclass instance should be entitled to override and extend the methods of the superclass instance thus generated. It seems unambiguous to allow this to happen without repeating the instance Mutter Something. So we'd have class Monad f where (=) :: f s - (s - f t) - f t instance Applicative f where ff * fs = ff = \ f - fs = \ s - return (f s) and we'd still be able to write instance Monad Maybe where return = Just -- completing the generated Applicative Just s = f = f s Nothing = _ = Nothing and acquire Monad, Applicative, Functor. No new instance inference semantics is required. In order to transform code under this proposal to code acceptable now, one need only keep track of which methods belong to which class and which classes have default superclass instances: each compound instance can then be split into its individual components before compilation under the current rules. Is this clear? Does it seem plausible? All the best Conor ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Functor hierarchy proposal and class system extension proposal
Hi Ben On 4 Jan 2011, at 19:19, Ben Millwood wrote: On Tue, Jan 4, 2011 at 1:21 PM, Conor McBride co...@strictlypositive.org wrote: Jón's proposal was to improve the latter situation by allowing the subclass to specify a default (partial) implementation of a superclass. So we might write This, on its own, is not quite enough. For one thing, we need a way to switch it off. I should certainly be permitted to write something like instance Applicative Blah where return = ... (*) = ... hiding instance Functor Blah The use of 'hiding' here I'd object to, as it really isn't a good description of what's going on. It's perhaps suboptimal. I chose hiding only because it's already a vaguely keywordy thing. It's only syntax. What's important is... Personally I'd think it more clear to explicitly opt into an automatic instance: instance Applicative Blah where return = ... (*) = ... deriving (Functor) -- or something like that [..] but I think there is an argument to be made about how much of this process we want to be explicit and how much we want to be implicit. ...the argument about what should be implicit or explicit, opt-in or opt-out. In this argument, I disagree with you. I'd much rather it was notationally cheaper to go with the supplied default, provided deviation from the default is also fairly cheap (but explicit). My plan also has the advantage of cheaper backward compatibility (for this and other (future) class splittings). Note that in my example, return had moved to Applicative, pure had been dumped, and a typical Monad instance would look like instance Monad Maybe where Just x = f = f x Nothing = _ = Nothing return = Just -- where this implicitly opts into and extends the -- Applicative instance -- and also implicitly generates Functor We could not simply have said deriving Applicative here, because the default instance is incomplete. In general, one might want to override some but not all of the default instance, just as one does when default method implementations come from the class. There's a general engineering concern as well. The refactoring cost of splitting Applicative off as a lesser version of Monad, taking return, adding (*) derivable from (=) is much reduced by this choice. I'm sure it's not the only instance of a class we might discover is better split: the opt-in default reduces inertia to such design improvements. I'd certainly be happy with a different opt-out notation, but I would be unhappy if opting in (and overriding/extending) were made more complex than necessary to allow an opt-out default. All the best Conor ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
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] 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 mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[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
[Haskell] Scottish Category Theory Seminar
*** Scottish Category Theory Seminar *** First Meeting *** Friday 27 November 2009, 2pm *** University of Glasgow, Scotland Dear All, We are pleased to announce the first meeting of the Scottish Category Theory Seminar which will be a forum for discussion of all aspects of category they, be they straight category theory or applications to computer science or physics etc. We envisage meeting for an afternoon once every few months, at some congenial location in Scotland. Talks by Scots and by visitors are welcome. Please contact us if you would like to host a meeting or give a talk. Meetings are open, and all are welcome to attend. The first meeting will take on Friday 27 November at the University of Glasgow at 2pm. At the first meeting, we are pleased to announce the following invited speakers * Martin Hyland, Universty of Cambridge * Nicola Gambino, University of Palermo * Alexander Kurz, University of Leicester * Willem Bernard Heijltjes, University of Edinburgh This meeting will receive financial support from the Complex Systems Engineering theme of SICSA, the Scottish Informatics and Computer Science Alliance and from the Department of Mathematics at the University of Glasgow. More details can be found at http://personal.cis.strath.ac.uk/~ng/sct.html If you wish to attend, or want more information about the Scottish Category Theory Seminar, please email scotc...@cis.strath.ac.uk Neil Ghani Tom Leinster Alex Simpson ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
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] 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 mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[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
