Re: (Succ Haskell') `and` $ dependent types
On Sun, Jul 15, 2007 at 09:04:16AM +1200, Vivian McPhail wrote: Hello, As the authors point out [1], coal-face time needs to be expended before real world adoption of Dependently-Typed functional programming. But let's get the ball rolling. They say that haskell programmers are normally averse to dependent types. Is this true? It seems to me that one of the appeals of Haskell is the ability to program in a prove perfect, write once (elegant) style. Is not dependent typing a good move towards this goal?. It addresses a problem [2] with which we, in our everyday common inter-hominem usage, can deal -- with which (ideal) Haskell should deal. While the major Haskell implementations would require a substantial overhaul, the change at the syntactic level appears to be minimal. There also needs to be advance with respect to programmer development (automatic edit-time inference of (some) types). What are peoples' thoughts on adding dependent types to haskell as a non-incremental evolutionary step? Does the haskell community want to stick with conservative additions to Haskell and a static base, or does the haskell community want to stay in step with the best theoretical developments? Vivian [1] http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html [2] http://thread.gmane.org/gmane.comp.lang.haskell.cafe/21314 Dependant types aren't new, they're ten times older than Haskell ;) I don't even think that adding dependant types to Haskell would be that hard. Most of the needed infrastructure (notably the binder rule, lexically scoped type variables, and explicit instantiation) already exists in the implementation of rank-N types in GHC. I think much of the work would be in revising Core (currently it uses a variant of Barandregt's λω, which is strictly less powerful (IIUC) than the full dependant λC) and flattening the typeinfer/kindinfer staging. Of course, since Haskell is not strongly normalizing, we would not be able to use a calculus where applications of CONV are implicit. Interaction with qualified types (type classes, MPTC, fundeps, implicit parameters, extensible records, associated type synonym equality predicates, etc) could be interesting, in both senses of the word. Stefan signature.asc Description: Digital signature ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: [Haskell-cafe] Haskell's prefix exprs
On Mon, Jul 09, 2007 at 03:55:52PM +0200, Christian Maeder wrote:
Hi,
I would like haskell to accept the following (currently illegal)
expressions as syntactically valid prefix applications:
f = id \ _ - []
g = id let x = [] in x
h = id case [] of [] - []
i = id do []
j = id if True then [] else []
The rational is that expressions starting with a keyword should extend
as far as possible (to the right and over several lines within their
layout).
In this case the above right hand sides (rhs) are unique juxtapositions
of two expressions. (This extension should of course apply to more than
two expressions, i. e. f a do [])
Furthermore the above rhs are all valid if written as infix expressions:
f = id $ \ _ - []
g = id $ let x = [] in x
h = id $ case [] of [] - []
i = id $ do []
j = id $ if True then [] else []
False.
f = runST $ do return ()
is a type error.
f = runST (do return ())
is legal.
So your proposal isn't as pointless as you think :)
(In fact, maybe for haskell-prime $ could be changed to a keyword.)
Does this pose any problems that I haven't considered?
Not that I know of. Indeed, the status quo is a (minor) pain to parse,
and in my Haskell compiler project I *wanted* to implement your
proposal.
I think only more (and shorter) illegal haskell programs will become legal.
Cheers Christian
Maybe someone else can work out the details for Haskell's grammar
Not hard at all. In http://haskell.org/onlinereport/syntax-iso.html,
change:
exp^10 - \ apat[1] ... apat[n] - exp (lambda abstraction, n=1)
| let decls in exp (let expression)
| if exp then exp else exp (conditional)
| case exp of { alts } (case expression)
| do { stmts } (do expression)
| fexp
fexp - [fexp] aexp (function application)
aexp - qvar (variable)
| gcon (general constructor)
| literal
| ( exp )(parenthesized expression)
| ( exp[1] , ... , exp[k] ) (tuple, k=2)
| [ exp[1] , ... , exp[k] ] (list, k=1)
| [ exp[1] [, exp[2]] .. [exp[3]] ] (arithmetic sequence)
| [ exp | qual[1] , ... , qual[n] ] (list comprehension, n=1)
| ( exp^i+1 qop^(a,i) ) (left section)
| ( lexp^i qop^(l,i) ) (left section)
| ( qop^(a,i)[-] exp^i+1 ) (right section)
| ( qop^(r,i)[-] rexp^i ) (right section)
| qcon { fbind[1] , ... , fbind[n] } (labeled construction,
n=0)
| aexp[qcon] { fbind[1] , ... , fbind[n] } (labeled update, n = 1)
to:
exp^10 - [exp^10] aexp(function application)
aexp - \ apat[1] ... apat[n] - exp (lambda abstraction, n=1)
| let decls in exp (let expression)
| if exp then exp else exp (conditional)
| case exp of { alts } (case expression)
| do { stmts } (do expression)
| qvar (variable)
| gcon (general constructor)
| literal
| ( exp )(parenthesized expression)
| ( exp[1] , ... , exp[k] ) (tuple, k=2)
| [ exp[1] , ... , exp[k] ] (list, k=1)
| [ exp[1] [, exp[2]] .. [exp[3]] ] (arithmetic sequence)
| [ exp | qual[1] , ... , qual[n] ] (list comprehension, n=1)
| ( exp^i+1 qop^(a,i) ) (left section)
| ( lexp^i qop^(l,i) ) (left section)
| ( qop^(a,i)[-] exp^i+1 ) (right section)
| ( qop^(r,i)[-] rexp^i ) (right section)
| qcon { fbind[1] , ... , fbind[n] } (labeled construction,
n=0)
| aexp[qcon] { fbind[1] , ... , fbind[n] } (labeled update, n = 1)
All new ambiguities are resolved adequately by the let/lambda meta rule.
(I've posted this message to glasgow-haskell-users before, but it
applies to every Haskell implementation and should be discussed here.)
haskell-prime@haskell.org would be even better.
Stefan
signature.asc
Description: Digital signature
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Nested pattern binding translates to outermost binding?
On Fri, Jul 06, 2007 at 06:20:45PM -0700, Dave Bayer wrote: On Jul 6, 2007, at 1:46 PM, Stefan O'Rear wrote: You could have just used -ddump-ds... Core is way more readable than GHC assembly. Great suggestion! Core looks familiar from playing with template Haskell, is it identical? No, Core is much lower level. It does not have guards, where-blocks, list comprehensions, type classes, etc; everything is reduced to simple pattern bindings, lambdas, lets, applications, and unboxed literals. Can one / does anyone use Core as a target for experimental toy languages? Aside from the moving target caveats... Apparently not, since GHC's support for *reading* core has been broken since the 6.0 days with nary a complaint. (Aaron Tomb and Tim Chevalier are currently working on fixing it). Stefan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Newbie proposal: operator backquoting
On Mon, Jun 25, 2007 at 03:46:19PM +0100, Ian Lynagh wrote: On Thu, Jun 21, 2007 at 09:14:55AM +0400, Dusty wrote: foo '-'1 has two arguments, (-) and 1,while foo -1 has one argument, -1 As *I* understood this, foo - 1 would not change. In fact except for the new `varsym` and `consym` forms, the grammer would not change. How would this break existing code? Thanks Ian, a member of the Out with DMR, defaulting, unary negation and n+k patterns club Ian: what's DMR? Stefan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Apparent contradiction in H98 prescribed behavior of 'data X = (:+){ x :: Int, y :: Int } deriving(Show)'
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:
[EMAIL PROTECTED]:/tmp$ cat Main.hs
data X = (:*) { x :: Int, y :: Int } deriving(Show)
main = print ((:*) 2 2)
[EMAIL PROTECTED]:/tmp$ runghc Main.hs
(:*) {x = 2, y = 2}
[EMAIL PROTECTED]:/tmp$ runhugs Main.hs
:* {x = 2, y = 2}
[EMAIL PROTECTED]:/tmp$ yhc Main.hs
Compiling Main ( Main.hs )
[EMAIL PROTECTED]:/tmp$ yhi Main.hbc
2 :* 2
[EMAIL PROTECTED]:/tmp$
Note that the hugs output for this corner case is unparseable and thus
buggy!
Stefan
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
