[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.
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
More information about the Haskell-Cafe
mailing list