[Haskell-cafe] Re: Type-level arithmetic

Martin Sulzmann sulzmann at comp.nus.edu.sg
Sun Oct 21 21:14:02 EDT 2007

Manuel M T Chakravarty writes:
 > 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.

Explained slightly differently.

The above type function is open (hence, we only apply matching)
whereas in functional logic programming type functions are closed
(therefore, we use unification/residuation).

Such an approach fits well together with "open" type classes as found
in Haskell.


 > 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.
 > _______________________________________________
 > Haskell-Cafe mailing list
 > Haskell-Cafe at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list