Slides have gone up

[paulcc]

I've converted my presentation to simple Html, and you can now get it
from the supermondays site:
http://www.supermondays.org/wp-content/uploads/2009/02/taste.html

Paul

[Alex Kavanagh]

Hi Paul

paulcc wrote, On 11/02/09 07:21:

>
> I've converted my presentation to simple Html, and you can now get it
> from the supermondays site:
> http://www.supermondays.org/wp-content/uploads/2009/02/taste.html

Thanks for putting that up.

Cheers
Alex.

>
> Paul
>
> >

[Paul Callaghan]

I feel the need to explain the "where's the type error" slide...

The point is: most static type systems, even ones like Haskell's, are still relatively crude and won't catch big classes of programmer error.

But, there are now several technologies which can be used to catch many more things at compile time (and thus reduce the need for run-time checks or intensive testing).

One of these is "dependent types". To cut a long story short, we can talk about features of the data _as part of_ their types, and usefully exploit the extra information.

Example: the type of an array can include size information as well as base element type.

Lookup then gets a more detailed type, eg

[Paul Callaghan]

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.

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!

Paul

[Alex Kavanagh]

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.

Alex.

>
> Paul
>
>
>
> >

--
Alex Kavanagh
Tinwood Ltd -- Open Source Information & Communications Solutions
Delivering Freedom, Creating Value
w: www.tinwood.com
e: alex.k...@tinwood.com
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.