[Fun-thursday] Slides: A Brief Intro. to Dependently Typed Programming

[suhorng Y]

Hello:

Just wanna make sure.
In the sorting example, we gave it the type

    sort : (xs : [N]) -> \exists ( \ys -> Perm xs ys * Ordered ys )

Similarly, in the maximum function, we have the type

    max : (xs : [N]) -> (xs /= []) -> \exists ( Sup xs )

and `Sup xs` is also a function.

Why wouldn't we give the proof directly, but rather uses
assertions that when given a parameter, tries to (re-?)construct
the proof?

suhorng

2013/9/6 Shin-Cheng Mu <scm at iis.sinica.edu.tw>

> Dear friends,
>
> These are my slides yesterday,
> "A Brief Intro. to Dependently Typed Programming"
>
> http://pc-scm.iis.sinica.edu.tw/FT20130905.pdf
>
> sincerely,
> Shin
> scm at iis.sinica.edu.tw
>
>
>
> _______________________________________________
> Fun-thursday mailing list
> Fun-thursday at iis.sinica.edu.tw
> http://www.iis.sinica.edu.tw/mailman/listinfo/fun-thursday
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.iis.sinica.edu.tw/pipermail/fun-thursday/attachments/20130907/1d2214a6/attachment.html>