Python is lazier than Haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
30 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Python is lazier than Haskell

Henning Thielemann

I like to apply for the quote of the week. :-)

   "If Haskell is great because of its laziness,
    then Python must be even greater,
    since it is lazy at the type level."

Dynamically typed languages only check types if they have to, that is if
expressions are actually computed. Does this prove that laziness at type
level as in Python is a great thing or does this prove that laziness at
the value level as in Haskell is a bad thing or does this prove nothing?

Hope for controversial discussion ...

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Vo Minh Thu
2011/4/27 Henning Thielemann <[hidden email]>:

>
> I like to apply for the quote of the week. :-)
>
>  "If Haskell is great because of its laziness,
>   then Python must be even greater,
>   since it is lazy at the type level."
>
> Dynamically typed languages only check types if they have to, that is if
> expressions are actually computed. Does this prove that laziness at type
> level as in Python is a great thing or does this prove that laziness at the
> value level as in Haskell is a bad thing or does this prove nothing?
>
> Hope for controversial discussion ...

I like the sloth to be eager to eat my bugs.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Ketil Malde-5
In reply to this post by Henning Thielemann
Henning Thielemann <[hidden email]> writes:

> I like to apply for the quote of the week. :-)
>
>   "If Haskell is great because of its laziness,
>    then Python must be even greater,
>    since it is lazy at the type level."

Well, this is indeed (an elegant reformulation of) a common objection,
namely that Python programmers often want to run code that is *wrong*,
in ways that a statically typed languge would prohibit.  The idea being
that during development, you can test a partial program without worrying
about the missing pieces from - or pieces that don't quite fit - the
puzzle.

In Haskell, I often need to add stubs of "undefined" in order to do
this.  I don't mind, since it is often very useful to say *something*
about the particular piece - e.g. I add the type signature, establishing
the shape of the missing piece without bothering with the actual
implementation just yet.

That "Haskell is great because of its laziness" is arguable, see Robert
Harper's blog for all the arguing. (http://existentialtype.wordpress.com/)

-k
--
If I haven't seen further, it is by standing in the footprints of giants

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Serguey Zefirov
2011/4/27 Ketil Malde <[hidden email]>:
> Henning Thielemann <[hidden email]> writes:
> That "Haskell is great because of its laziness" is arguable, see Robert
> Harper's blog for all the arguing. (http://existentialtype.wordpress.com/)

I think that author sin't quite right there.

http://en.wikipedia.org/wiki/Haskell_%28programming_language%29
Haskell (pronounced /ˈhæskəl/) is a standardized, general-purpose
purely functional programming language, with *non-strict* semantics
and strong static typing.

Haskell is great because of non-strictness.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Thomas Davie
In reply to this post by Henning Thielemann

On 27 Apr 2011, at 10:30, Henning Thielemann wrote:

>
> I like to apply for the quote of the week. :-)
>
>  "If Haskell is great because of its laziness,
>   then Python must be even greater,
>   since it is lazy at the type level."
>
> Dynamically typed languages only check types if they have to, that is if expressions are actually computed. Does this prove that laziness at type level as in Python is a great thing or does this prove that laziness at the value level as in Haskell is a bad thing or does this prove nothing?
>
> Hope for controversial discussion ...

To add to the points various other people have made...

This completely misses what laziness gives Haskell – it gives a way of completing a smaller number of computations than it otherwise would have to at run time.  The hope being that this speeds up the calculation of the result after the overhead of laziness is taken into account.

Computing types lazily does not do this – it means that instead of computing the types at compile time and doing *nothing* at runtime, we now do some computation at runtime.  Not only that but we introduce more bugs.

So laziness in computation takes us from doing *all* computation to doing a subset at runtime.
laziness in typing takes us from doing *no* computation to doing a subset of all at runtime.

Doesn't look quite so rosy now does it :)

Bob
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Tony Morris-4
On 27/04/11 20:02, Thomas Davie wrote:
> This completely misses what laziness gives Haskell – it gives a way of completing a smaller number of computations than it otherwise would have to at run time.  The hope being that this speeds up the calculation of the result after the overhead of laziness is taken into account.
This is not what laziness gives us. Rather, it gives us terminating
programs that would otherwise not terminate.

--
Tony Morris
http://tmorris.net/



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

MigMit
In reply to this post by Henning Thielemann
It would be, if only it checked the (necessary) types during compile time. As it is now, it seems like a claim that C is lazy just because any pointer can be null.

Отправлено с iPhone

Apr 27, 2011, в 13:30, Henning Thielemann <[hidden email]> написал(а):

>
> I like to apply for the quote of the week. :-)
>
>  "If Haskell is great because of its laziness,
>   then Python must be even greater,
>   since it is lazy at the type level."
>
> Dynamically typed languages only check types if they have to, that is if expressions are actually computed. Does this prove that laziness at type level as in Python is a great thing or does this prove that laziness at the value level as in Haskell is a bad thing or does this prove nothing?
>
> Hope for controversial discussion ...
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Felipe Lessa
2011/4/27 MigMit <[hidden email]>:
> It would be, if only it checked the (necessary) types during compile time. As it is now, it seems like a claim that C is lazy just because any pointer can be null.

Strictness analysis is only an optimization, you don't need it to be
lazy in the term-level.

However Python does check the kinds, the types of the types, at
compile-time.  Everything is *.  ;-)

Cheers,

--
Felipe.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Jerzy Karczmarczuk
In reply to this post by Tony Morris-4

> Thomas Davie wrote:
>> This completely misses what laziness gives Haskell – it gives a way of completing a smaller number of computations than it otherwise would have to at run time. (...)
Tony Morris continues the ping-pong:
> This is not what laziness gives us. Rather, it gives us terminating
> programs that would otherwise not terminate.
Next, please...

You know, this suggests that you should read the parable of Blind Men
and the Elephant.

Alright, my turn. I never wanted to write non-terminating programs (what
for?), and all my programs executed exactly those instructions they
should have executed, not more or less. I see ONE usage of laziness: the
possibility to write co-recursive equations, which become algorithms.
The possibility to represent processes as "data", which makes it easier
to reason upon them. Do we really need some dogmatic specification of
laziness?...

Jerzy Karczmarczuk


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Alexander Solla


On Wed, Apr 27, 2011 at 6:07 AM, Jerzy Karczmarczuk <[hidden email]> wrote:

Thomas Davie wrote:
This completely misses what laziness gives Haskell – it gives a way of completing a smaller number of computations than it otherwise would have to at run time. (...)
Tony Morris continues the ping-pong:

This is not what laziness gives us. Rather, it gives us terminating
programs that would otherwise not terminate.
Next, please...

You know, this suggests that you should read the parable of Blind Men and the Elephant.

Alright, my turn. I never wanted to write non-terminating programs (what for?),

Daemons/servers/console interfaces/streaming clients?  

In any case, this question is opposite to the one you "should" be asking.  Laziness makes "infinite" programs finite.  We can express infinite data structures and compute them lazily, as necessary for the completion of the "greater" program.  This would not be possible using simple expressive forms, in other languages.
 
and all my programs executed exactly those instructions they should have executed, not more or less.

I would rather write equations describing what things "are" than instructions on how to compute them.  In the end, these are the same, and yet we can still use referential transparency and the other functional concepts to their fullest.
 
I see ONE usage of laziness: the possibility to write co-recursive equations, which become algorithms

What about "infinite" lists?  There is no need for mutually recursive functions to see the usefulness of a list which never ends, and is computed to the length that your algorithm /acutally/ requires.

For example, the function "intIndex" (using tuple-types for convenience):

intIndex :: [a] -> I.IntMap a
intIndex list = I.fromAscList $ zip (,) [0..] list

Laziness allows simpler expression, and is not necessary for mutual recursion.  For example, we can implement mutual recursion in C with goto, and that language model uses "imperative evaluation" -- evaluation of instructions in the order they are given.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Jerzy Karczmarczuk
Alexander Solla comments my comment :

Alright, my turn. I never wanted to write non-terminating programs (what for?),

Daemons/servers/console interfaces/streaming clients?  
Come on, not THIS kind of non-termination. This has little to do with strictness/laziness, I think. Endless loops can be coded in various ways...
 
I see ONE usage of laziness: the possibility to write co-recursive equations, which become algorithms

What about "infinite" lists?  There is no need for mutually recursive functions to see the usefulness of a list which never ends, and is computed to the length that your algorithm /acutally/ requires.

This is almost EXACTLY what I meant. When I say "co-recursive", I do not mean "mutually recursive". Rather the extrapolating recursion, not necessarily "terminating" (lacking the base clause) but finitely progressing, such as the standard definition of the stream of integers, used to scare the beginners...

ints = 1 : zipWith (+)  (fix (1:)) ints
  where  fix f = f (fix f)

Thanks.

Jerzy Karczmarczuk


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

serialhex
so, as a n00b to haskell i can't say much about its laziness, and not knowing much about how python works i'm about the same there.  though i do know ruby, and afaik ruby doesn't _care_ what type something is, just if it can do something.  example from the rails framework:

#-------
class NilClass  # nil is mostly equivalent to c's NULL
  def blank?
    true
  end
end

class String
  def blank?
    self.size == 0
  end
end

["", "person", nil].each do |element|
  puts element unless element.blank?
end
#-------

the output of course would simply be "person", but that's not the object of my post.  in ruby they use what some call "duck typing"  if it looks like a duck and quacks like a duck... it's a duck.  unlike in most other programming languages where you have to draw blood in order to check if it's a duck (i mean, it could be a goose for all we know, and we all know what geese do to our programs...)  and while this programming style might be useful in this (and many other) contexts, there are probably a bunch of others where it only gets in the way.

also, in case you are wondering... haskell is going to be the second language i delve into.  i've already started ruby and will have to un-learn a bunch of things because of that from what i read, but i find a number of haskells features to be interesting.  and hey, it's a new way to think about problems right?
hex

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Albert Y. C. Lai
In reply to this post by Henning Thielemann
On 11-04-27 05:30 AM, Henning Thielemann wrote:
> I like to apply for the quote of the week. :-)
>
> "If Haskell is great because of its laziness,
> then Python must be even greater,
> since it is lazy at the type level."

Using Data.Dynamic, Haskell has a story for laziness at the type level, too.

Haskell has:
value-level lazy, can opt-out
type-level lazy, can opt-in
continuations, can opt-in

Python has:
value-level eager, no choice
type-level lazy, no choice
no continuations, no choice

If Python type laziness were that great, why isn't it rich in type-level
programs? Has anyone even added numbers in Python at the type level?

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Gracjan Polak
In reply to this post by Ketil Malde-5
Ketil Malde <ketil <at> malde.org> writes:
>
> In Haskell, I often need to add stubs of "undefined" in order to do
> this.  I don't mind, since it is often very useful to say *something*
> about the particular piece - e.g. I add the type signature, establishing
> the shape of the missing piece without bothering with the actual
> implementation just yet.

Seconded.

Sometimes I wish for a -fphp flag that would turn some type errors into
warnings. Example:

v.hs:8:6:
    Couldn't match expected type `[a]' against inferred type `()'
    In the first argument of `a', namely `y'
    In the expression: a y
    In the definition of `c': c = a y

GHC could substitute 'y = error "Couldn't match expected type `[a]' against
inferred type `()'"' and compile anyway.

Would that bring Haskell closer to Python?

--
Gracjan



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Ertugrul Söylemez
Gracjan Polak <[hidden email]> wrote:

> Ketil Malde <ketil <at> malde.org> writes:
>
> > In Haskell, I often need to add stubs of "undefined" in order to do
> > this.  I don't mind, since it is often very useful to say
> > *something* about the particular piece - e.g. I add the type
> > signature, establishing the shape of the missing piece without
> > bothering with the actual implementation just yet.
>
> Seconded.

I don't see any problem with this.  Although I usually have a bottom-up
approach, so I don't do this too often, it doesn't hurt, when I have to.


> Sometimes I wish for a -fphp flag that would turn some type errors
> into warnings. Example:
>
> v.hs:8:6:
>     Couldn't match expected type `[a]' against inferred type `()'
>     In the first argument of `a', namely `y'
>     In the expression: a y
>     In the definition of `c': c = a y
>
> GHC could substitute 'y = error "Couldn't match expected type `[a]'
> against inferred type `()'"' and compile anyway.
>
> Would that bring Haskell closer to Python?

It would make people abuse that feature.  I don't want it.  Haskell is
so difficult to abuse compared to other languages, and I'd like to keep
it that way.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Chris Smith-31


On Apr 28, 2011 9:25 AM, "Ertugrul Soeylemez" <[hidden email]> wrote:
>
>
> > Sometimes I wish for a -fphp flag that would turn some type errors
> > into warnings. Example:
> >
> > v.hs:8:6:
> >     Couldn't match expected type `[a]' against inferred type `()'
> >     In the first argument of `a', namely `y'
> >     In the expression: a y
> >     In the definition of `c': c = a y
> >
> > GHC could substitute 'y = error "Couldn't match expected type `[a]'
> > against inferred type `()'"' and compile anyway.
> >
> > Would that bring Haskell closer to Python?
>
> It would make people abuse that feature.  I don't want it.

I do, particularly in GHCi.  I don't mind if Haskell refuses to build a binary, but having to comment out coded in order to load bits in GHCi is definitely a pain.

--
Chris Smith


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

James Cook
In reply to this post by Ertugrul Söylemez

On Apr 28, 2011, at 11:27 AM, Ertugrul Soeylemez wrote:

> Gracjan Polak <[hidden email]> wrote:
>
>> Ketil Malde <ketil <at> malde.org> writes:
>>
>>> In Haskell, I often need to add stubs of "undefined" in order to do
>>> this.  I don't mind, since it is often very useful to say
>>> *something* about the particular piece - e.g. I add the type
>>> signature, establishing the shape of the missing piece without
>>> bothering with the actual implementation just yet.
>>
>> Seconded.
>
> I don't see any problem with this.  Although I usually have a bottom-
> up
> approach, so I don't do this too often, it doesn't hurt, when I have  
> to.
>

Agreed - in fact, I have always thought of this style of coding as one  
of the truly great things about Haskell, and was surprised to see it  
presented as a negative.  The idea of that being a burden had never  
even entered my mind.

The fact that I can say "foo = undefined" and go about my business as  
if foo were, in fact, an existing component, is nice.  But as you  
point out, that can be done in pretty much any dynamically typed  
language just as trivially.   The truly great thing about it is that I  
can also say "foo :: (Bar a, Num b) => a -> b -> (qux -> m baz) -> f m  
(x, Either q g)", etc., and the compiler can then tell me when I  
misuse this *entirely fictitious* entity.   Or, when I'm done writing  
my code that uses foo, I can say "foo :: ()" and let the compiler  
errors tell me what sort of a creature I have asked "foo" to be.  Or,  
I can just start coding "foo" and let the compiler tell me whether  
what I do is consistent with how I've used it elsewhere.

>
>> Sometimes I wish for a -fphp flag that would turn some type errors
>> into warnings. Example:
>>
>> v.hs:8:6:
>>    Couldn't match expected type `[a]' against inferred type `()'
>>    In the first argument of `a', namely `y'
>>    In the expression: a y
>>    In the definition of `c': c = a y
>>
>> GHC could substitute 'y = error "Couldn't match expected type `[a]'
>> against inferred type `()'"' and compile anyway.
>>
>> Would that bring Haskell closer to Python?
>
> It would make people abuse that feature.  I don't want it.  Haskell is
> so difficult to abuse compared to other languages, and I'd like to  
> keep
> it that way.

Maybe, but it should be easy to make sure that you aren't using any  
code that abuses it; just make sure you compile all your stuff with  
that flag explicitly turned off - any code that "abuses" it would  
simply fail to build.  I'd expect to be able to do that by setting "-
fno-php" as a global ghc-option in the cabal config file.  I'd  
probably also advocate making that flag switch type errors to non-
suppressible warnings (that is, do not provide any way whatsoever in  
the compiler to make those warnings silent).

On a related note, I think that this sort of a feature would not  
really get at the usual objection about strong static typing  
incorrectly rejecting valid programs.  All this does is change it so  
that such programs are, instead of being rejected, altered to throw  
runtime errors in cases that could actually have worked but the type  
system was not expressive enough to prove.  It would give what I think  
of as the worst of both worlds:  Programs that can never work would be  
allowed to slip past the compiler, and programs that could work if the  
type system were smarter still won't work.

I think the proper thing to do would be to translate such code into  
code that uses Dynamic, or more likely some generalization of it.  It  
would require some serious thought about how to deal with polymorphic  
types, and especially ones that involve type classes.  All in all, it  
seems to me that a full correct implementation of such a system would  
essentially amount to embedding a full Haskell interpreter in the  
compiled executable.

Done right, though, it could be a pretty nice feature.  If nothing  
else, it would let you experiment extensively in a nice safe little  
sandbox to gain confidence in your dangerous untypeable code before  
you "take the plunge" and use unsafeCoerce.

-- James

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Albert Y. C. Lai
In reply to this post by serialhex
On 11-04-27 05:44 PM, serialhex wrote:
> in ruby they use what some call "duck typing"  if it looks
> like a duck and quacks like a duck... it's a duck.

Python and Javascript also do duck typing.

Haskell does Functor typing. A Functor is something that provides an
"fmap" method. List does it, so you can do

   fmap not [True,False]

Maybe also does it, so you can also do

   fmap not (Just False)

Your own data type could also do it. Suppose your data type is (binary tree)

   data BT a = Z | Y a (BT a) (BT a)
     deriving Show

then you add

   instance Functor BT where
     fmap f Z = Z
     fmap f (Y x t0 t1) = Y (f x) (fmap f t0) (fmap f t1)

then BT provides an "fmap" method too, and so you can also do

   fmap not (Y True (Y False Z Z) Z)

If it fmaps like a Functor, it is a Functor. That is Functor typing.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

Dan Doel
In reply to this post by Ertugrul Söylemez
(Sorry if you get this twice, Ertugrul; and if I reply to top. I'm
stuck with the gmail interface and I'm not used to it.)

On Thu, Apr 28, 2011 at 11:27 AM, Ertugrul Soeylemez <[hidden email]> wrote:
> I don't see any problem with this.  Although I usually have a bottom-up
> approach, so I don't do this too often, it doesn't hurt, when I have to.

I do. It's low tech and inconvenient.

Whenever I program in Haskell, I miss Agda's editing features, where I
can write:

   foo : Signature
   foo x y z = ?

Then compile the file. The ? stands in for a term of any type, and
becomes a 'hole' in my code. The editing environment will then tell me
what type of term I have to fill into the hole, and give me
information on what is available in the scope. Then I can write:

   foo x y z = { partialImpl ? ? }

and execute another command. The compiler will make sure that
'partialImpl ? ?' has the right type to fill in the hole (with ?s
again standing in for terms of arbitrary type). If the type checking
goes through, it expands into:

   foo x y z = partialImpl { } { }

and the process repeats until my function is completely written. And
of course, let's not forget the command for automatically going from:

   foo x y z = { x }

to

   foo Con1 y z = { }
   foo Con2 y z = { }
   foo Con3 y z = { }
   ...

I don't think there's anything particularly Agda-specific to the
above. In fact, the inference required should be easier with
Haskell/GHC. Features like this would be pretty killer to have for
Haskell development; then I wouldn't have to prototype in Agda. :)

-- Dan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Python is lazier than Haskell

austin seipp-3
Dan,

I believe there was some work on this functionality for GHC some time
ago (agda-like goals for GHC, where ? in agda merely becomes
'undefined' in haskell.) See:

https://github.com/sebastiaanvisser/ghc-goals

This work was done a few years ago during a hackathon (the 09 Utrecht
hackathon.) There is a frontend-executable providing goal information,
as well as a patch to GHC to support it. It was never integrated into
GHC and was left dead in the water essentially (for exactly what
reasons, I do not know.)

I find myself using the 'undefined' trick somewhat often as well. I'm
not very familiar with agda, but familiar enough to have seen goals
before in the interactive emacs mode, and I think this would be a nice
feature for people who find themselves doing similar things.

On Thu, Apr 28, 2011 at 3:18 PM, Dan Doel <[hidden email]> wrote:

> (Sorry if you get this twice, Ertugrul; and if I reply to top. I'm
> stuck with the gmail interface and I'm not used to it.)
>
> On Thu, Apr 28, 2011 at 11:27 AM, Ertugrul Soeylemez <[hidden email]> wrote:
>> I don't see any problem with this.  Although I usually have a bottom-up
>> approach, so I don't do this too often, it doesn't hurt, when I have to.
>
> I do. It's low tech and inconvenient.
>
> Whenever I program in Haskell, I miss Agda's editing features, where I
> can write:
>
>    foo : Signature
>    foo x y z = ?
>
> Then compile the file. The ? stands in for a term of any type, and
> becomes a 'hole' in my code. The editing environment will then tell me
> what type of term I have to fill into the hole, and give me
> information on what is available in the scope. Then I can write:
>
>    foo x y z = { partialImpl ? ? }
>
> and execute another command. The compiler will make sure that
> 'partialImpl ? ?' has the right type to fill in the hole (with ?s
> again standing in for terms of arbitrary type). If the type checking
> goes through, it expands into:
>
>    foo x y z = partialImpl { } { }
>
> and the process repeats until my function is completely written. And
> of course, let's not forget the command for automatically going from:
>
>    foo x y z = { x }
>
> to
>
>    foo Con1 y z = { }
>    foo Con2 y z = { }
>    foo Con3 y z = { }
>    ...
>
> I don't think there's anything particularly Agda-specific to the
> above. In fact, the inference required should be easier with
> Haskell/GHC. Features like this would be pretty killer to have for
> Haskell development; then I wouldn't have to prototype in Agda. :)
>
> -- Dan
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



--
Regards,
Austin

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12