[Haskell-cafe] Re: Type-level arithmetic

[Manuel M T Chakravarty]

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.

Manuel

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.