Re: Decidable type systems? (WAS: Associated TypeSynonyms question)

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

Re: Decidable type systems? (WAS: Associated TypeSynonyms question)

greenrd
Miles Sabin <[hidden email]> wrote:

> Can someone explain to me why decidability is of any practical
> interest at all? procedure which might never terminate and one which might take
> 1,000,000 years to terminate? Actually, why push it out to 1,000,000
> years: in the context of a compiler for a practical programming
> language, a decision procedure which might take an hour to terminate
> might as well be undecidable

But are there any decidable type checking algorithms that have been
seriously proposed or used which would take far too long to terminate
for real code? If not, then decidability is the only thing that matters.
--
Robin
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Decidable type systems? (WAS: Associated TypeSynonyms question)

Miles Sabin
Robin Green wrote,
> But are there any decidable type checking algorithms that have been
> seriously proposed or used which would take far too long to terminate
> for real code? If not, then decidability is the only thing that
> matters.

Surely what matters is that they don't take far too long to terminate!

Cheers,


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

Re: Decidable type systems? (WAS: Associated TypeSynonyms question)

Tomasz Zielonka
In reply to this post by greenrd
On Thu, Feb 16, 2006 at 12:27:54PM +0000, Robin Green wrote:
> But are there any decidable type checking algorithms that have been
> seriously proposed or used which would take far too long to terminate
> for real code? If not, then decidability is the only thing that matters.

Perhaps they weren't proposed because decidability was not the only
thing that mattered?

Best regards
Tomasz

--
I am searching for programmers who are good at least in
(Haskell || ML) && (Linux || FreeBSD || math)
for work in Warsaw, Poland
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe