[Haskell] Class-parameterized classes, and the type-level logarithm
We show invertible, terminating, 3-place addition, multiplication, and
exponentiation relations on type-level Peano numerals, where _any_ two
operands determine the third. We also show the invertible factorial
relation. This gives us all common arithmetic operations on Peano
numerals, including n-base discrete logarithm, n-th root, and the
inverse of factorial. The inverting method can work with any
representation of (type-level) numerals, binary or decimal.
Furthermore, the inverter itself is generic: it is a type-class
function, that is, a type-class parameterized by the type-class to
`invert'. There has been a proposal on Haskell' to give equal rights
to types and classes. In Haskell98+multi-parameter type classes,
classes are already first-class, for all practical purposes. We can
quite easily define (potentially, higher-order) type functions on type
classes.
Ashley Yakeley wrote:
] I know for the usual Peano representation of natural numbers, at least,
] it's possible to represent addition and subtraction with a single class
] with two fundeps (because classes represent relations between types
] rather than functions on them).
That can be done even for decimal type numerals,
cf. number-parameterized-types paper. But we can do better: we can
have _three_ functional dependencies, so that any two operands of the
type class determine the third. The key insight was the result of a
conversation with Chung-chieh Shan and Gregory Price in the evening of
Nov 10, 2003.
Despite what the extension says, the arithmetic relations in this file
are all decidable.
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module PeanoArithm where
>
> data Z
> data S a
> __ = __
First we define a semi-sum relation, with only two functional
dependencies:
> class Sum2 a b c | a b -> c, a c -> b
> instance Sum2 Z a a
> instance Sum2 a b c => Sum2 (S a) b (S c)
Now we add the third dependency. It is that simple.
> class Sum a b c | a b -> c, a c -> b, b c -> a
> instance (Sum2 a b c, Sum2 b a c) => Sum a b c
After defining a few numbers,
> add:: Sum a b c => a -> b -> c
> add = __
>
> type One = S Z
> type Two = S (S Z)
>
> zero = __ :: Z
> one = __ :: One
> two = __ :: Two
> three = add one two
> n4= add two two
we see that the typechecker can indeed add and subtract:
> ta1 = \x -> (add three x `asTypeOf` three)
> ta2 = \x -> (add x two `asTypeOf` three)
> -- ta3 = \x -> (add three x `asTypeOf` two) -- fails
*PeanoArithm> :t ta1
ta1 :: Z -> S (S (S Z))
*PeanoArithm> :t ta2
ta2 :: S Z -> S (S (S Z))
Before we move to products, we introduce a few utilities
> class NLE x y
> instance Sum2 x a y => NLE x y
>
> class Mul a b c | a b -> c -- a single-dependency multiplication
> instance Mul Z b Z
> instance (Mul a b c', Sum c' b c) => Mul (S a) b c -- (a+1)*b = a*b + b
The relation |NLE x y| holds if |x| is less or equal to |y|, that is,
there exists a numeral |a| that in sum with |x| gives |y|.
We now introduce the generic inverter of an arithmetic function defined
on the whole set of natural numbers. The inverter is parameterized by
the numeric function (that is, a type class) to invert. We define
the type of these classes by the following class. It maps types to
classes (see also the HList paper):
> class Registry clas a b c | clas a b -> c
The inverter, the type-class function, is so trivial that I'm ashamed
to discuss it. It is a simple for-loop.
> class Inv clas init limit a b c | clas init a b -> c
> instance (NLE x limit, Registry clas x b a', Sum2 a' r a,
> Inv' r clas x limit a b c)
> => Inv clas x limit a b c
> class Inv' r clas x limit a b c | r clas x a b -> c
> instance Inv' Z clas x limit a b x-- Found it
> instance Inv clas (S x) limit a b c -- try next x
> => Inv' (S r) clas x limit a b c
Division is defined as an inverse of multiplication:
> data RegMul
> instance Mul a b c => Registry RegMul a b c
>
> class Div m n q | m n -> q -- m = n * q
> instance Inv RegMul Z m m n q => Div m n q
We partially apply Inv to the right operands, and get the Div relation
in return.
> pdiv :: Div a b c => a -> b -> c
> pdiv = __
>
> -- Only where all dependencies exist...
> class Product a b c | a b -> c, a c -> b, b c -> a
> instance (Mul a b c, Div c b a, Div c a b) => Product a b c
>
> prod:: Product a b c => a -> b -> c
> prod = __
Now the typechecker can multiply and divide
> n6 = prod two three
> tm1 = \x -> (prod three x `asTypeOf` n6)
> tm2 = \x -> (prod x two `asTypeOf` n6)
> -- tm3 = \x -> (prod x n4 `asTypeOf` n6)
> tm4 = \x -> (prod x n6 `asTypeOf` n6)
> -- tm5 = \x -> (prod x zero `asTypeOf` n6)
> tm6 = \x -> (prod x zero `asTypeOf` zero)
The inferred types are
tm1 :: S (S Z) -> S (S (S (S (S (S Z)
tm2 :: S (S (S Z)) -> S (S (S (S (S (S Z)
tm4 :: S Z -> S (S (S (S (S (S Z)
The commented-out tests raise type errors.
The exponenti
Re: [Haskell] Type synonyms in the instance head
Am Donnerstag, 2. Februar 2006 21:48 schrieb Mads Lindstrøm: > [...] > Also what the type synonym is synonym for, may not have any name and > thus properly not be telling at all, as in: > > type TellingName a = \a -> String What is \a -> String? > /Mads Lindstrøm Best wishes, Wolfgang ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] RULE 2006 at FLoC --- paper deadline 14 May
== Call for Papers RULE 2006 7th International Workshop on Rule-Based Programming http://www.dcs.kcl.ac.uk/events/RULE06/ Seattle, USA 11th August 2006 A satellite event of RTA 2006 at FLoC === The basic concepts of rule-based programming appear throughout Computer Science, from theoretical foundations to practical implementations. Term rewriting is used in semantics in order to describe the meaning of programming languages, as well as in the implementation of program transformation systems. Rules are used implicitly or explicitly to perform computations, e.g., in Mathematica, OBJ, ELAN, Maude or to perform deductions, e.g., by using inference rules to describe or implement a logic, theorem prover or constraint solver. Mail clients and mail servers use complex rules to help users organising their email and sorting out spam. Language implementations use bottom-up rewrite systems for code generation (as in the BURG family of tools.) Constraint-handling rules (CHRs) are used to specify and implement constraint-based algorithms and applications. Rule-based programming idioms also give rise to multi-paradigm languages like Claire. The purpose of this workshop is to bring together researchers from the various communities working on rule-based programming to foster advances in the theory of rule-based programming, cross-fertilization between theory and practice, research on rule-based programming methods, and the exploration of important application domains of rule-based programming. RULE 2006 will be a one-day satellite event of RTA 2006 at FLoC. Topics of interest -- * Languages for rule-based programming - Expressive power, Idioms, Design patterns - Semantics, Type systems - Implementation techniques - System descriptions * Other foundations - Complexity results - Advances on rewriting logic - Advances on rewriting calculus - Static analyses of rule-based programs - Transformation of rule-based programs * Applications of rule-based programming, e.g.: - Program transformation - Software analysis and generation - System Control - Work-flow control - Knowledge engineering - System descriptions * Combination with other paradigms - Functional programming - Logic programming - OO programming - Biocomputing - Language extensions - Language embeddings Submissions and Publication: Papers (of at most 15 pages) should be submitted electronically via the submission page: http://www.easychair.org/RULE2006 Any problems with the submission procedure should be reported to one of the PC chairs: [EMAIL PROTECTED], [EMAIL PROTECTED] Accepted papers will be published in the preliminary proceedings volume, which will be available during the workshop. The final proceedings will be published in Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier. IMPORTANT DATES - 14th May 2006: Deadline for electronic submission of papers - 15th June 2006: Notification of acceptance of papers - 30th June 2006: Deadline for final versions of accepted papers - 11th August 2006: Workshop Programme Committee: - Mark van den Brand (TU Eindhoven, Netherlands) - Horatiu Cirstea (LORIA, France) - Pierre Deransart (INRIA Rocquencourt, France) - Michael L. Collard (Kent State University, USA) - Martin Erwig (Oregon State University, USA) - Francois Fages (INRIA Rocquencourt, France) - Maribel Fernandez (Co-Chair, King's College London, UK) - Jean-Pierre Jouannaud (LIX, Ecole Polytechnique, France) - Oleg Kiselyov (FNMOC, USA) - Ralf Laemmel (Co-Chair, Microsoft, USA ) - Ugo Montanari (Universita di Pisa, Italy) - Pierre-Etienne Moreau (LORIA, France) - Tobias Nipkow (Technical University Munich, Germany) - Tom Schrijvers (K.U.Leuven, Belgium) - Martin Sulzmann (National University of Singapore, Singapore) - Victor Winter (University of Nebraska at Omaha, USA) ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Type synonyms in the instance head
Mads Lindstrøm wrote: "You cannot, for example, write: type P a = [[a]] instance Monad P where ... This design decision is independent of all the others, and easily reversed, but it makes sense to me." It's not clear to me how this can be reversed. Wouldn't reversing this mean introducing "type lambda", and doesn't that raise all kinds of nasty issues (like having to type-annotate function applications)? If I have: data LongAndUglyName a = ... type ShortAndTellingName a = LongAndUglyName a It seems to make sensible to: instance Foo ShortAndTellingName You can do this instead: type ShortAndTellingName = LongAndUglyName -- Ashley Yakeley ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Type synonyms in the instance head
Hi all In this url http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#id3144979 one can read about "Type synonyms in the instance head". A quote: "You cannot, for example, write: type P a = [[a]] instance Monad P where ... This design decision is independent of all the others, and easily reversed, but it makes sense to me." It does not make sense to me! Could anybody explain why this makes sense? Below, I will try to explain why it does not make sense to me. If I have: data LongAndUglyName a = ... type ShortAndTellingName a = LongAndUglyName a It seems to make sensible to: instance Foo ShortAndTellingName Also it is called a type _synonym_ and the type synonym and what it is synonym for, should therefore be interchangeable. This restriction do not only apply to instance heads, but also to contexts, as in: instance (Foo LongAndUgleName) => class something ... Here again LongAndUglyName cannot be replaced by ShortAndTellingName. This can be annoying if you have a lot of these instance declarations. Also what the type synonym is synonym for, may not have any name and thus properly not be telling at all, as in: type TellingName a = \a -> String /Mads Lindstrøm ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
