On Wed, 6 Feb 2008, Jonathan Cast wrote:
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote:
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked
function does
not terminate on the example input, then the function does not
On Thu, 7 Feb 2008, Neil Mitchell wrote:
Hi
I think what you want to say now is not just
(filter f l) is type correct when there is some argument on which f
returns true
but
(filter f l) is type correct when there is some *element of l* on
which f returns true
or in
Hello Henning,
Thursday, February 7, 2008, 12:29:02 AM, you wrote:
it's impossible to check for *arbitrary* function call whether it will be
terminated. seems that you don't have formal CS education? :)
so one can develop set of functions that are guaranteed to be
terminated or guaranteed
Hi
Indeed, if Catch or ESC or similar tools can handle such specifications it
would be great. However I suspect that the translation you gave is
different from what I wanted. I consider a function buggy, if it
implements 'const' considerably more complicated than just saying 'const'.
:-)
Hello Dan,
Thursday, February 7, 2008, 4:04:03 AM, you wrote:
I.e., it's not necessary to restrict the class of functions you consider
if you're willing to give up on full automation. So I disagree with the
only if below.
ok, read this as computer can ensure..., because it was exactly the
On Thu, 7 Feb 2008, Bulat Ziganshin wrote:
Thursday, February 7, 2008, 4:04:03 AM, you wrote:
I.e., it's not necessary to restrict the class of functions you consider
if you're willing to give up on full automation. So I disagree with the
only if below.
ok, read this as computer can
Hi Bulat,
Once again, let's be careful about what check arbitrary functions for
termination/non-trivialness means. If you mean, decide via an
algorithm whether a function is terminating on all inputs, then yes,
you need to restrict the class of functions. If you mean prove in some
logic that a
On Tue, 5 Feb 2008, Bulat Ziganshin wrote:
Hello Henning,
Tuesday, February 5, 2008, 6:01:27 PM, you wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
such
Hello Henning,
Wednesday, February 6, 2008, 5:09:56 PM, you wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
such things may be detected by (too) smart compiler,
On Wed, 6 Feb 2008, Bulat Ziganshin wrote:
Hello Henning,
Wednesday, February 6, 2008, 5:09:56 PM, you wrote:
Is Haskell's type system including extensions strong enough for
describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
Hello Henning,
Wednesday, February 6, 2008, 6:09:28 PM, you wrote:
it's another question: you can describe trivial values using type
system, but can't prohibit them using it - it's impossible because you
can't check for arbitrary algorithm whether it will be finally stopped
I could consider
On Wed, 6 Feb 2008, Bulat Ziganshin wrote:
Hello Henning,
Wednesday, February 6, 2008, 6:09:28 PM, you wrote:
it's another question: you can describe trivial values using type
system, but can't prohibit them using it - it's impossible because you
can't check for arbitrary algorithm
On Tue, 5 Feb 2008, Dan Licata wrote:
[CC'ed to the agda mailing list as well]
On Feb05, Henning Thielemann wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked function does
not terminate on the example input, then the function does not pass the
type check and as a compromise this would be ok.
Can't fault this logic. The problem is
Am Mittwoch, 6. Februar 2008 18:39 schrieb Bulat Ziganshin:
[…]
this means that answer to original question - one can ensure that
argument for filter is non-terminating function only if these
functions are written using some special notation which doesn't allow
to write arbitrary
On Feb06, Henning Thielemann wrote:
On Tue, 5 Feb 2008, Dan Licata wrote:
On Feb05, Henning Thielemann wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
Hi
I think what you want to say now is not just
(filter f l) is type correct when there is some argument on which f
returns true
but
(filter f l) is type correct when there is some *element of l* on
which f returns true
or in Haskell:
filterNonEmpty f x = assert (not $ null
Let's be careful here: decidability is only relevant if you want to
*automatically* prove calls to filter correct. It is certainly possible
to give a type system/specification logic for reasoning about all
functions written in a Turing-complete language (e.g., all Haskell
functions). In such a
On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote:
On Wednesday 06 February 2008, Henning Thielemann wrote:
If the type checker does not terminate because the checked
function does
not terminate on the example input, then the function does not
pass the
type check and as a compromise this
[CC'ed to the agda mailing list as well]
On Feb05, Henning Thielemann wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
will always compute an empty list. Using an
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
will always compute an empty list. Using an appropriate signature for
the function it shall be rejected at compile time, because
Hello Henning,
Tuesday, February 5, 2008, 6:01:27 PM, you wrote:
Is Haskell's type system including extensions strong enough for describing
a function, that does not always return a trivial value? E.g.
(filter (\x - x==1 x==2))
such things may be detected by (too) smart compiler, but in
22 matches
Mail list logo
