- Haskell-prime - Haskell.org

Re: Literate Haskell specification
by Vivian McPhail 24 Apr '07

24 Apr '07

Dear Committee If I recall correctly, in the tex-style literate haskell specification, code is delimited by a \begin{code} \end{code} This does not allow for multilanguage support in a single source file. It would be nice to have a single document in which we could mix English, Haskell, and, for example, Coq proofs. To this end, would it make more sense to delimit haskell code by \begin{haskell} \end{haskell} ? Cheers, Vivian Date: Fri, 06 Apr 2007 15:07:28 -0400 > From: Isaac Dupree <isaacdupree(a)charter.net> > Subject: Literate Haskell specification > To: haskell-prime(a)haskell.org > Message-ID: <46169A70.80909(a)charter.net> > Content-Type: text/plain; charset=ISO-8859-1 > > -----BEGIN PGP SIGNED MESSAGE----- > Hash: SHA1 > > As I brought up earlier in Haskell-cafe > http://thread.gmane.org/gmane.comp.lang.haskell.cafe/20026 > , the Haskell98 specification for literate haskell (report section 9.4) > could use some work, at least clarifications (existing haskell > implementations differ in some ways) - see that thread for details. > Since I haven't successfully gotten to writing a concrete revision of > that section, I thought I'd at least bring the issue to the attention of > specifically haskell-prime people, as it is an issue that "should > definitely" be addressed in the Report. Hopefully there's someone > around here who might tackle it :) > > > Good luck, > Isaac > -----BEGIN PGP SIGNATURE----- > Version: GnuPG v1.4.3 (GNU/Linux) > Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org > > iD8DBQFGFppvHgcxvIWYTTURAgoqAKDKFXaVBVeSfodzlgEte5Loy42unACfXfbl > qDlxnSUaNH5rg8r58KAkKl8= > =UVvx > -----END PGP SIGNATURE----- >

2 1

Why Mathematical Soundness Matters.
by Vivian McPhail 21 Apr '07

21 Apr '07

Hi All, This is in regard to previous posts about mathematical preludes. > class Set a > > class (Set s) => SemiGroup s o where > semigroup_op :: o -> (s,s) -> s > -- closure > -- associative > > class (SemiGroup s o) => Monoid s o where > identity :: o -> s > > class (Monoid s o) => Group s o where > inverse :: o -> s -> s > > class Optimisable a where > cost :: Set b => a -> b First, consider a semigroup, which is a set with an associative operation. Into this structure falls Matrices with multiplication. There is scope for optimisation of a series of multiplications. Inductively for each m1 * m2 * m3 compare the cost of m1 * m2 versus m2 * m3 which can be simply obtained from the size of the index of the matrix. Thus expressions like (14,3) x (3,15) x (15,2) can be computed as (14,3) x ((3,15) x (15,2)) and not in a more expensive way. Furthermore, if we tag identities with a phantom type, we can eliminate needless operations like 3 + 0. Not as much optimisation can be achieved with inverses (3 + -3) because it might be just as expensive to calculate that something is an inverse as to do actual calculation. So how can this optimisation be performed? Well this is a question that I put forward to you, Gentle Reader. Static: It seems to me that expressions the types of which are known at compile-time can be optimised by using type-level programming in combination with compiler rewrite rules, e.g. if we have a type class SizeLarger then the expression > semigroup_op (semigroup_op m1 m2) m3 can be rewritten as > semigroup_op m1 (semigroup_op m2 m3) depending upon the SizeLarger types of the various (semigroup_op _ _) function calls. Another method is to manipulate the expressions as ASTs and convert to the concrete using TH. But what about dynamic data? Dynamic: These are terms whose types are not known until run-time (such as would happen when loading an arbitrary matrix from a file). In this case we can't use compiler term-rewriting or TH, but what options are there? Depending upon the speed/complexity of type-checking versus computation would it not be feasible to use run-time type checking (a polymorphic Dynamic type) to achieve this optimisation? Yes there is a lot to said in favour of static type-checking, but there are cases in which it is not feasible, witness type-level bounds checking of run-time loaded matrices of unknown shape. In a program that used run-time typechecking (yes there would be a computational overhead) the dynamic stuff would be isolated from the 'trusted' statically checked program and values could only be injected through trusted entry points (e.g. get4SquareDoubleMatrix :: Dynamic -> IO (Array ((D4 $ Sz),(D4 $ Sz)) Double). In any case, writing 'simple' arithmetic expressions would become more cumbersome because of the overhead of annotating types and possibly moving between ASTs and the concrete. But if we a had collection of mathematically sound classes like SemiGroup, Monoid, Group, Field, etc... then these optimisations could be built into the compiler and we could sugar the programmer-side just as it has been for Monads. In conclusion, I put this forward as a reason for Mathematically Meaningful Numeric Classes and in obiter I am putting forward support for polymorphic Dynamic types (run-time typechecking). Cheers, Vivian

1 0

Relax the restriction on Bounded derivation
by Neil Mitchell 18 Apr '07

18 Apr '07

Hi, >From Section 10 of the Haskell report, regarding automatic derivation: to derive Bounded for a type: "the type must be either an enumeration (all constructors must be nullary) or have only one constructor." This seems a very artificial restriction - since it allows you to be in any one of two camps, but no where in between. It also means that Either doesn't derive Bounded, while it could easily do so: instance (Bounded a, Bounded b) => Bounded (Either a b) where minBound = Left minBound maxBound = Right maxBound So I propose that this restriction be lifted, and that the obvious extension be given such that minBound is the lowest constructor with a pile of minBounds, and maxBound is the highest constructor with a pile of maxBound. This proposal has been implemented in Derive: http://www-users.cs.york.ac.uk/~ndm/derive/ Thanks Neil

4 4

Apparent contradiction in H98 prescribed behavior of 'data X = (:+){ x :: Int, y :: Int } deriving(Show)'
by Stefan O'Rear 17 Apr '07

17 Apr '07

Given: data X = (:*){ x :: Int, y :: Int } deriving(Show) which is syntactically correct: > constr -> con { fielddecl[1] , ... , fielddecl[n] } (n>=0) > con -> ( consym ) and the following from 10.4: * If the constructor is defined to be an infix operator, then the derived Read instance will parse only infix applications of the constructor (not the prefix form). * If the constructor is defined using record syntax, the derived Read will parse only the record-syntax form, and furthermore, the fields must be given in the same order as the original declaration. the behavor of the Show instance seems to be contradicted, since :+ is an infix operator and is defined using record syntax. Suggested resolution: * If the constructor is defined using infix syntax, then the derived Read instance will parse only infix applications of the constructor (not the prefix form). Thus, 'data X = Int :+ Int' would show infix but 'data X = (:+) Int Int' would not. Alternatively, change the con in the above production for constr to conid, thus banning infix record constructors. Status: stefan@stefans:/tmp$ cat Main.hs data X = (:*) { x :: Int, y :: Int } deriving(Show) main = print ((:*) 2 2) stefan@stefans:/tmp$ runghc Main.hs (:*) {x = 2, y = 2} stefan@stefans:/tmp$ runhugs Main.hs :* {x = 2, y = 2} stefan@stefans:/tmp$ yhc Main.hs Compiling Main ( Main.hs ) stefan@stefans:/tmp$ yhi Main.hbc 2 :* 2 stefan@stefans:/tmp$ Note that the hugs output for this corner case is unparseable and thus buggy! Stefan

1 0

General pattern bindings
by Twan van Laarhoven 16 Apr '07

16 Apr '07

In the interest of removing things from the standard, I found this in the Haskell 98 report (section 4.4.3.2): > The general form of a pattern binding is p match, where a match is the > same structure as for function bindings above; in other words, a > pattern binding is: > > p | g1 = e1 > | g2 = e2 > ... > | gm = em > where { decls } I did not even know these things existed, is there anyone who actually uses general pattern bindings? If not, the question becomes whether removing these bindings would improve the language. It can be argued that it makes the language less consistent. Declarations would change from > decl -> (funlhs | pat0) rhs > rhs -> = exp [where decls] > | gdrhs [where decls] to something like > decl -> funlhs rhs > | pat0 srhs > srhs -> = exp [where decls] > rhs -> srhs > | gdrhs [where decls] On the other hand, we can remove most of section 4.3.2.2. Any opinions? Twan

5 4

Re: Mathematics in Haskell
by R Hayes 03 Apr '07

03 Apr '07

Wouldn't this be a good discussion for the Haskell Prime List? Reilly Hayes +1 415 388 3903 (office) +1 415 846 1827 (mobile) rfh(a)ridgecrestfinancial.com On Apr 2, 2007, at 3:24 PM, Andrzej Jaworski wrote: >> I too was put off by the Num issues though--strange mixture of >> sophisticated >> category theory and lack of a sensible hierarchy of algebraic >> objects. > > Perhaps we should replace CT with lattice theoretic thinking (e.g. > functor = monotonic > function) before cleaning up the type-related mess? > See: http://citeseer.ist.psu.edu/269479.html > >> so count me in on an effort to make Haskell more mathematical. >> For me that >> probably starts with the semigroup/group/ring setup, and good >> arbitrary-precision as well as approximate linear algebra support. > > I agree: semigoups like lattices are everywhere. > Then there could be a uniform treatment of linear algebra, > polynomial equations, operator > algebra, etc. So, perhaps haste is not a good advice here? > > -Andrzej > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe

1 0

strict bits of datatypes
by Ian Lynagh 22 Mar '07

22 Mar '07

Hi all, A while ago there was a discussion on haskell-cafe about the semantics of strict bits in datatypes that never reached a conclusion; I've checked with Malcolm and there is still disagreement about the right answer. The original thread is around here: http://www.haskell.org/pipermail/haskell-cafe/2006-October/018804.html but I will try to give all the relevant information in this message. The question is, given: data Fin a = FinCons a !(Fin a) | FinNil w = let q = FinCons 3 q in case q of FinCons i _ -> i is w 3 or _|_? ---------- The _|_ argument ---------- (Supporters include me, ghc and hugs) q = FinCons 3 q === (by Haskell 98 report 4.2.1/Strictness Flags/Translation q = (FinCons $ 3) $! q === (by definition of $, $!) q = q `seq` FinCons 3 q === (solution is least fixed point of the equation) q = _|_ Thus w = case _|_ of FinCons i _ -> i so w = _|_. ---------- The 3 argument ---------- (Supporters include Malcolm Wallace, nhc98 and yhc) Here I will just quote what Malcolm said in his original message: The definition of seq is seq _|_ b = _|_ seq a b = b, if a/= _|_ In the circular expression let q = FinCons 3 q in q it is clear that the second component of the FinCons constructor is not _|_ (it has at least a FinCons constructor), and therefore it does not matter what its full unfolding is. and in his recent e-mail to me: Yes, I still think this is a reasonable interpretation of the Report. I would phrase it as "After evaluating the constructor expression to WHNF, any strict fields contained in it are also be guaranteed to be in WHNF." This also makes q a fixpoint of q = q `seq` FinCons 3 q, but not the least fixed point. ---------- So I think it would be good if we can all agree on what the meaning should be, and then to clarify the wording in the report so that future readers understand it correctly too. Thanks Ian

14 23

type aliases and Id
by oleg＠pobox.com 22 Mar '07

22 Mar '07

Lennart Augustsson wrote: > Ganesh and I were discussing today what would happen if one adds Id > as a primitive type constructor. How much did you have to change the > type checker? Presumably if you need to unify 'm a' with 'a' you now > have to set m=Id. I wonder if this proposal is a good idea. Let us consider the following near-Haskell98 code > class C a > instance C (m a) > instance C Int (usually there will be constraints on m. We shall see a useful example of this in a moment). This code typechecks under slight and common relaxation of the rules on the form of instance head. That example will probably typecheck in Haskell'. Under the proposal that Id t === t, typechecking of this code will require overlapping instances, which quite unlikely to make it into Haskell' and is a quite significant and controversial extension. Speaking of overlapping instances, let's generalize the example to > class C a > instance C (m a) > instance C a It does typecheck in current Haskell. Under the Id proposal, this example will NOT typecheck, ever. This is because the two instances become exact duplicates. Indeed, every type that matches "a" will match "m a" (with m = Id) and vice versa. The two instances match the same class of types (that is, all of the types). Let us come back to our simple example and make it practical. > class C a where incr :: a -> a > > instance (C a, Functor m) => C (m a) where incr = fmap incr > instance C Int where incr = succ > > test = incr (Just [[[1::Int]]]) the example increments integers deeply embedded in some functorial data structures. The operations of this kind are requested from time to time on Haskell-Cafe. This code compiles and works (no overlapping or undecidable instances are required). Under the Id t === t proposal, this example will diverge (perhaps, it will diverge even in the compiler). The reason is that the base case cannot be reached; the type Int can always be considered as Id Int and so the first instance will apply again.

2 1

type aliases and Id
by Ian Lynagh 21 Mar '07

21 Mar '07

Hi all, Suppose I have a datatype: data Foo a = Foo { int :: a Int, char :: a Char } where I start off with (Foo Nothing Nothing) :: Foo Maybe, gradually accumulate values until I have (Foo (Just 5) (Just 'c')), and then I want to remove the Maybe type so I can lose all the now-redundant Just constructors. Well, suppose in actual fact I prefer the name "CanBe" to Maybe. Then for the first part I want type CanBe a = Maybe a foo :: Foo CanBe foo = ... but of course this fails because CanBe is a non-fully-applied type synonym in "foo :: Foo CanBe", and I can fix this by eta-reducing thus: type CanBe = Maybe foo :: Foo CanBe foo = ... Now for the second part I want type Id a = a foo' :: Foo Id foo' = ... but again Id is not fully applied. However, this time I cannot eta-reduce it! "type Id =" is a parse error, as is "type Id". I'd really like to be able to define an eta-reduced Id; I see two possibilities: * Allow "type Id =" (I prefer this to "type Id" as I think we are more likely to want to use the latter syntax for something else later on). * Implementations should eta-reduce all type synonyms as much as possible, e.g. type T a b c d = X a b Int c d is equivalent to type T a b = X a b Int and type Id a = a is equivalent to a type that cannot be expressed directly. Any opinions? Thanks Ian

8 10

Re: [GHC] #1215: GHC fails to respect the maximal munch rule while lexing "qualified reservedids"
by Ian Lynagh 14 Mar '07

14 Mar '07

Context if you haven't been following: http://hackage.haskell.org/trac/ghc/ticket/1215 On Tue, Mar 13, 2007 at 03:12:33PM -0000, GHC wrote: > > Interesting. It turns out I misinterpreted the Haskell lexical syntax: > GHC lexes `M.default` as `M` `.` `default`, because `M.default` is not a > valid qvarid but I neglected to take into account the maximal munch rule. > > We have an open ticket for Haskell' about this: > http://hackage.haskell.org/cgi-bin/haskell-prime/trac.cgi/wiki/QualifiedIde… > which was until just now > inaccurate (I've now fixed it). I propose to fix GHC in 6.8 to match the > Haskell' proposal. If I understand correctly then the proposal would make e.g. foo = Bar.where a syntactically valid program, but one which would be guaranteed to fail to compile with a not-in-scope error? Wouldn't it be cleaner for it to be a lexical error? Unfortunately I'm not sure how to say this in the grammar; the best I can come up with is: program -> {lexeme | whitespace | error } error -> [ modid . ] reservedid Thanks Ian

2 1