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.