Paul,
You raise an interesting tangential question. Are languages like Agda not even remotely mainstream?
Regards,
Balthazar
On Tue, Jun 16, 2009 at 3:32 PM, Paul Phillips
<paulp@...> wrote:
On Tue, Jun 16, 2009 at 03:24:10PM -0700, Balthazar Crowley wrote:
> Thanks for the response. Unfortunately, that expression does not
> denote a type. And the type of the thing it does denote is not what is
> required.
Oh, it sounds like you want a dependent type.
That is, the type "Array[Char] of length 140." Right?
http://en.wikipedia.org/wiki/Dependent_type
You can't have that in scala or any remotely mainstream language, but it
is one of my fonder hopes for the future.
--
Paul Phillips | We act as though comfort and luxury were the chief
Vivid | requirements of life, when all that we need to make us
Empiricist | really happy is something to be enthusiastic about.
i pull his palp! | -- Charles Kingsley
--
Balthazar Crowley
Resident Magician
DSLver.com
