Type Checking Type Classes

[Tobias . Nipkow]

The following paper, to be presented at POPL93, is now available by ftp:
  
Tobias Nipkow and Christian Prehofer
 Type Checking Type Classes

We study the type inference problem for a system with type classes as in the
functional programming language Haskell. Type classes are an extension of
ML-style polymorphism with overloading. We generalize Milner's work on
polymorphism by introducing a separate context constraining the type
variables in a typing judgement. This leads to simple type inference systems
and algorithms which closely resemble those for ML. In particular we present
a new unification algorithm which is an extension of syntactic unification
with constraint solving. The existence of principal types follows from an
analysis of this unification algorithm.

File: lehrstuhl/nipkow/popl93.dvi.Z
Machine: ftp.informatik.tu-muenchen.de / 131.159.0.110

Cyclic Types

[Tobias . Nipkow]

Lennart Augustsson writes:

 I thought there were problems with extending Hindley-Milner type systems
 with cyclic types:  The type inference can handle type correct programs,
 but will loop for certain type incorrect programs, or am I mistaken?

It is absolutely unproblematic to extend  Hindley-Milner type systems with
cyclic types, provided you use the right unification algorithm (ie you don't
just leave out the occurs-check as in some Prologs). However, in the
resulting system any closed lambda-term without constants has a type, in
particular \x.(x x). This kind of type system is implemented in Stefan Kaes'
Sample language.

Tobias

[Haskell-cafe] Gaussian elimination

[Tobias Nipkow]

Hi, I came up with the following extremely compact version of Gaussian
elimination for matrices represented as functions. I searched the web
but found nothing resembling it, probably because of its inefficiency.
Has anybody seen something like it before?

Thanks
Tobias

gauss :: Int - (Int - Int - Rational) - Maybe (Int - Int - Rational)
gauss 0 a = Just a
gauss (n+1) a =
  case dropWhile (\i - a i n == 0) [0..n] of
[] - Nothing
(k:_) -
  let ak' j = a k j / a k n
  a' i = if i == k then ak' else (\j - a i j - a i n * ak' j)
  in gauss n (swap k n a')

swap :: Int - Int - (Int - a) - (Int - a)
swap k n f = g
  where g x | x == k = f n
| x == n = f k
| otherwise = f x

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe