[Haskell-cafe] Re: Type-level arithmetic
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Fri Oct 19 08:46:09 EDT 2007
Ross Paterson wrote,
> On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote:
>> Lennart Augustsson wrote,
>>> And Haskell embedded a logical programming language on accident.
>> Well, we are just trying to fix that :)
> Since types are inferred using unification, and classes are still present,
> adding functions yields a functional logic programming language at the
> type level.
I used to agree with that, but I changed my opinion. Or more
precisely, I'd say that it is a very weak functional logic language.
"Weak" in the sense that it's logic component is essential nil.
Let me justify this statement. We have type variables that are like
"logical variables" in logic programming languages. However, we
never use function definitions to guess values for type variables.
Instead, function evaluation simplify suspends when it depends on an
uninstantiated variable and resumes when this variable becomes
instantiated. (The functional logic people call this evaluation
strategy "residuation".) For example, if we have
type family T a
type instance T Int = Char
then, given (T a ~ Char), we do *not* execute T backwards and infer
(a = Int). Instead, we leave (T a ~ Char) as it is and evaluate 'T'
only when 'a' becomes fixed.
There have been proposals for truely functional logic languages
using residuation, but they include support for backtracking and
producing multiple solutions to a single query. We support neither
on the type level.
So, the only interaction between type functions and unification left
is that function evaluation suspends on uninstantiated type
variables and resumes when they become instantiated. This is not
functional logic programming, it is *concurrent* functional
programming with single-assignment variables. In fact, languages
such as Id and pH, which are routinely characterised as concurrent
functional, use exactly this model.
I don't think the presence of type classes *without* functional
dependencies changes this.
PS: You get a *real* functional logic language by truly performing
unification modulo an equational theory. This leads to the
concept of E-unification and, in our constructor-based context,
to "narrowing" as an evaluation strategy.
More information about the Haskell-Cafe