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