[Haskell-cafe] Type System Trix was Re: Specify array or list size?

[Shae Matijs Erisson]

Daniel Carrera <dcarrera at digitaldistribution.com> writes:

> Is there a way to tell Haskell that a list or array must have exactly (say)
> 256 elements? I'd love to have Haskell make sure that the array I build is
> the correct size.

Yes, you can build lists with a maximum size.
The simplest approach I've seen is BoundedList.hs in the HaskellDB library:
http://cvs.sourceforge.net/viewcvs.py/haskelldb/haskelldb/src/Database/HaskellDB/

The more general question is, "How to encode values into types in such a way
that I can use them?"

One neat answer is here:
http://pobox.com/~oleg/ftp/Haskell/number-parameterized-types.html

There are a bunch of neat type tricks like this, but the next step up in
encoding information in types is dependent type systems like the one used in
Epigram: http://www.dur.ac.uk/CARG/epigram/

I recently asked on http://lambda-the-ultimate.org/ what else can be done with
type systems other than program safety.
I got a neat answer from David Teller:

<quote>
Static type-checking in Camelot guarantees RAM usage -- not only its safety but
also its amount.

Static type-checking in my controlled pi-calculus (definitely not a real
programming language) guarantees statically properties of access control ("only
X can use the printer", "I can only read this information for the purpose of
transferring it to you", ...) or resource management ("this program will never
require more than x threads, y RAM and z printers").

Static type-checking in TyPiCal guarantees the respect of some protocols. In
Acute, you can check the safety of communications...
</quote>

Type systems can do a lot of neat stuff these days, I've been able to use
HaskellDB in my paying work already!
-- 
It seems I've been living two lives. One life is a self-employed web developer
In the other life, I'm shapr, functional programmer.  | www.ScannedInAvian.com
One of these lives has futures (and subcontinuations!)|  --Shae Matijs Erisson