The Coq mailing list

[Roland Zumkeller <roland.zumkeller AT gmail.com>]

Hi Luke,

Polynomials in n variables can be represented as nested lists of depth
n, e.g the list of lists [[1,2],[3,4,5]] stands for (x,y) -> (y+2y) +
x * (3+4y+5y^2).

Their Coq datatype would be:

Fixpoint ply (n:nat) : Type := match n with
| O    => Q
| S n' => list (ply n')
end.

Addition of polynomials can be defined like this:

Fixpoint add n : ply n -> ply n -> ply n :=
match n as n0 return ply n0 -> ply n0 -> ply n0 with
| O    => Qplus
| S n' => map2 (add n')
end.

Here Coq allows us not to explain how to add a number to a list.
Simpler type systems force us to use trees instead of nested lists,
which makes operations a bit more acrobatic (for the Haskell
equivalent of the above code see
http://code.google.com/p/sergei/source/browse/trunk/src/Ply.lhs).

Best,

Roland


On Tue, Apr 14, 2009 at 8:59 AM, Luke Palmer 
<lrpalmer AT gmail.com>
 wrote:
> I'm going to be giving a presentation to a local functional programming
> group about dependent types.  Does anyone know of a potent, realistic
> example of (executable) code which is type safe, but does not look type safe
> to most type systems?
> I have a few contrived examples in mind, but I was wondering if there is a
> standard motivating example which is particularly poignant.
> Thanks,
> Luke



-- 
http://roland.zumkeller.googlepages.com/