coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Roland Zumkeller <roland.zumkeller AT gmail.com>
- To: Luke Palmer <lrpalmer AT gmail.com>
- Cc: coq-club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Examples of dependent type programming
- Date: Tue, 14 Apr 2009 23:35:57 -0400
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=Y9R3t2yUDQFKYIbLs7JovUbVpYGeMavL1rYES2W5Jd5PxU43j63D5vy0LL8lQQuhA4 8N6vhSGNcnobc0WCNQV2oSFIuBS8a53wabJo/Uc7ckf5KN4pejRB38KUbJ67x+4OCrav yqlC96cfs7lYQ6pJvUlZfE4rAaAfaL9OTM+o0=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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/
- [Coq-Club] Examples of dependent type programming, Luke Palmer
- Re: [Coq-Club] Examples of dependent type programming, Adam Chlipala
- Re: [Coq-Club] Examples of dependent type programming, Frederic Blanqui
- Re: [Coq-Club] Examples of dependent type programming, Roland Zumkeller
Archive powered by MhonArc 2.6.16.