Curry: An Integrated Functional Logic Language

Abstract

ion: A[x/τ ] ` e :: τ ′ A ` \x->e :: τ → τ ′ if τ is a type expression Existential: A[x/τ ] ` e :: Success A ` let x free in e :: Success if τ is a type expression Conditional: A ` e1 :: Bool A ` e2 :: τ A ` e3 :: τ A ` if e1 then e2 else e3 :: τ Figure 1: Typing rules for Curry programs equivalent to a type expression). A function type declaration f::τ is considered as an assignment of the type scheme ∀α1, . . . , αn.τ to f , where α1, . . . , αn are all type variables occurring in τ . The type τ is called a generic instance of the type scheme ∀α1, . . . , αn.τ ′ if there is a substitution σ = {α1 7→ τ1, . . . , αn 7→ τn} on the types with σ(τ ′) = τ . The types of all defined functions are collected in a type environment A which is a mapping from identifiers to type schemes. It contains at least the type schemes of the defined functions and an assignment of types for some local variables. An expression e is well-typed and has type τ w.r.t. a type environment A if A ` e :: τ is derivable according to the inference rules shown in Figure 1. A defining equation f t1 . . . tn = e [where x free] is well-typed w.r.t. a type environment A if A(f) = ∀α1, . . . , αm.τ [and A(x) is a type expression] and A ` \t1-> · · · \tn->e :: τ is derivable according to the above inference rules. A conditional equation l | c = r is considered (for the purpose of typing) as syntactic sugar for l = cond c r where cond is a new function with type scheme A(cond) = ∀α.Success→ α→ α. A program is well-typed if all its rules are well-typed with a unique assignment of type schemes to defined functions.10 Note that the following recursive definition is a well-typed Curry program according to the definition above (and the type definitions given in the prelude, cf. Appendix B): f :: [a] -> [a] f x = if length x == 0 then fst (g x x) else x g :: [a] -> [b] -> ([a],[b]) g x y = (f x, f y) h :: ([Int],[Bool]) h = g [3,4] [True,False] However, if the type declaration for g is omitted, the usual type inference algorithms are not able Here we assume that all local declarations are eliminated by the transformations described in Appendix D.8.