Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Examples of dependent type programming

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Examples of dependent type programming


chronological Thread 
  • 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/





Archive powered by MhonArc 2.6.16.

Top of Page