Paul Callaghan wrote, On 11/02/09 10:48:
> oops! was in vi mode then.
> Example: the type of an array can include size information as well
> as base element type.
> Lookup then gets a more detailed type, eg
> get : (n:Nat)Array a n -> (m :Nat) Prf(m < n) -> a
> which means, for all arrays of size n, we can get the m'th element if we
> supply evidence that m is less than n. Such evidence is easy to get, eg
> if we're looping over an array's contents, then the looping construct
> can easily guarantee that the current index is valid. Often, creation of
> this evidence can be automated too by a bit of automatic theorem proving
> in an IDE.
I'm not sure what you are getting at here. I currently don't understand
the syntax for Haskell as I haven't (yet) picked up the book on it!
> Notice that this means we eliminate bad array references completely at
> compile time.
> Now, this mechanism can be used to embed all kinds of info in the type
> level, even logical invariants (eg balanced tree). It's an interesting area!
Interesting but complex and completely opaque to me! I really need to
get into this a bit more.
Tinwood Ltd -- Open Source Information & Communications Solutions
Delivering Freedom, Creating Value
a: 20 Sefton Ave, NE6 5QR, Company No: 5233914 (Eng & Wales), VAT No: GB
874 8669 54
Sorry if you got this by mistake - please accept our apologies;
please let us know that this message has gone astray so we don't
do it again. Thanks.