[TYPES] Declarative vs imperative

[Kalani Thielen]

At the risk of proving that this subject is just bikeshedding ...

Is it possible to say that "declarative" knowledge is the type-level-N+1 expression describing a level-N term (so it's meaningful relative to a particular term -- as in your example, machine code is itself "declarative" with respect to physical machines)?  Maybe you'd have to import dependent types / staged-programming to make that meaningful, but I think that's the right direction.

The prototypical example that I think of when I hear "declarative" is the square-root problem from SICP.  If you look at it now, it almost looks like they give a dependent type to Newton's method.


-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Rishiyur Nikhil
Sent: Monday, April 22, 2013 11:53 AM
To: Vladimir Lifschitz
Cc: types-list at lists.seas.upenn.edu
Subject: Re: [TYPES] Declarative vs imperative

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

>    ... fully declarative, like functional programming.
>    Here is how I would characterize the difference between procedural and
>    imperative programming.  A program in an imperative language 
> describes
an
>    algortithm.  A program in a declarative language describes a
specification.

But one man's specification is another man's algorithm.  Even in Haskell, one writes a sorting program typically by choosing a particular algorithm (heap sort, quick sort, ...).  Sure, these can be considered specifications of sorting, but they are hardly the most abstract spec for sorting.

Similarly, a C program is a specification for a hundred different machine code algorithms that manage memory, register allocation etc.

Nikhil