[Haskell-cafe] Re: Type-level arithmetic

[Martin Sulzmann]

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.

Martin



 > 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