[TYPES] Declarative vs imperative
kthielen at liquidnet.com
Mon Apr 22 12:16:18 EDT 2013
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.
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
> algortithm. A program in a declarative language describes a
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.
More information about the Types-list