- Glasgow-haskell-users

Parallel forkOS does not work on ubuntu
by Hoang Truong 10 Dec '08

10 Dec '08

Hello everybody, I am following "A Tutorial on Parallel and Concurrent Programming in Haskell" and I have a problem with making Haskell to use my multi-cores (Core 2 Quad CPU). The Haskel version I used is GHC 6.10.1, for Haskell 98. I compile my below program with command: ghc --make -threaded -debug thread0.hs, and run with: thread0 +RTS -N4 while watching the cpu usage on another terminal (by: mpstat -P ALL 1 100), but the program uses only one core of my Ubuntu Linux. Do any of you know why or has any suggestions? Below is my program: import Control.Concurrent import Control.Concurrent.MVar fib :: Int -> Int fib 0 = 0 fib 1 = 1 fib n = fib (n-1) + fib (n-2) dowork = putStrLn ("fib 35 = " ++ (show (fib 35))) threadA :: MVar Int -> MVar Int -> MVar Int -> IO () threadA valueToSendMVar valueToReadMVar valueToQuit = do -- some work dowork -- perform rendezvous putMVar valueToSendMVar 30 -- send value v <- takeMVar valueToReadMVar putStrLn ("result, fib 30 = " ++ (show v)) dowork -- notify done putMVar valueToQuit 0 -- send value threadB :: MVar Int -> MVar Int -> MVar Int -> IO () threadB valueToReceiveMVar valueToSendMVar valueToQuit = do -- some work dowork -- perform rendezvous by waiting z <- takeMVar valueToReceiveMVar putMVar valueToSendMVar (fib z) -- continue with other work dowork -- notify done putMVar valueToQuit 0 -- send value main :: IO () main = do aQuitA <- newEmptyMVar aQuitB <- newEmptyMVar aMVar <- newEmptyMVar bMVar <- newEmptyMVar forkOS (threadA aMVar bMVar aQuitA ) forkOS (threadB aMVar bMVar aQuitB ) -- wait for threadA and threadB takeMVar aQuitA takeMVar aQuitB return () Thanks a lot, Hoang

4 7

ghci linker and circular dependencies: bug or feature?
by Andrea Rossato 10 Dec '08

10 Dec '08

Hello, this is a followup of this: http://article.gmane.org/gmane.comp.lang.haskell.cafe/48644 which didn't have replays. In order to make the review a bit easier I prepared a minimal test case which, I believe, could prove there's a bug in the ghci linker. I'm not submitting a bug report because I'm not familiar with these problems and, in order not to waste other people's time, I'd rather have some preliminary review. All the code examples can be found here: http://gorgias.mine.nu/ffi-test/ Here a tarball of everything: http://gorgias.mine.nu/ffi-test.tar.gz Take a simple C library like this: #include <stdio.h> extern char my_var[]; void my_fun() { fprintf (stderr, "%s\n", my_var); } Since my_var is defined as external, the dynamic library compiled and linked with: gcc -Wall -fPIC -c -o mylib.o mylib.c gcc -shared -Wl,-soname,libmylib.so.1 -o libmylib.so.1.0 mylib.o would have my_var as undefined. If I write some Haskell bindings (Test.hsc) like this: module Test where import Foreign.C import Foreign #include <mylib.h> foreign import ccall unsafe "my_fun" my_cfun :: IO () my_fun :: IO () my_fun = my_cfun I'll need to include a stub.c file to initialize my_var: char my_var[] = "Hello World!!"; And now come my problems: 1. First I have a Cabal problem. If I set: extra-libraries: mylib this will be used also when compiling dist/build/Test_hsc_make, and, since libmylib.so.1.0 has an undefined reference to my_var, which will be initialized only later, by stub.c, the compilation of the bindings will fail with: Configuring mylib-0.1... Preprocessing library mylib-0.1... /tmp/ffi-test/libmylib.so: undefined reference to `my_var' collect2: ld returned 1 exit status linking dist/build/Test_hsc_make.o failed command was: /usr/bin/gcc -L/tmp/ffi-test -lmylib -L/usr/lib/ghc-6.10.1/base-4.0.0.0 [...] I can find a work-around by not setting cabal extra-libraries and instead setting ghc-options: -lmylib But when compiling a test file: import Test main = my_fun I'll need to pass -lmylib to ghc --make. 2. I also have ghci problem. If I try with: ghci test_lib.hs GHCi, version 6.10.1: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. Ok, modules loaded: Main. Prelude Main> main Loading package mylib-0.1 ... linking ... <interactive>: /home/andrea/.cabal/lib/mylib-0.1/ghc-6.10.1/HSmylib-0.1.o: unknown symbol `my_fun' ghc: unable to load package `mylib-0.1' Now, I have to remember to pass -lmylib: ghci -lmylib test_lib.hs GHCi, version 6.10.1: http://www.haskell.org/ghc/ :? for help Loading object (dynamic) mylib ... failed. <command line>: user specified .o/.so/.DLL could not be loaded (/tmp/ffi-test/libmylib.so: undefined symbol: my_var) Whilst trying to load: (dynamic) mylib Additional directories searched: (none) Now, the my_var symbol is included in: /home/andrea/.cabal/lib/mylib-0.1/ghc-6.10.1/HSmylib-0.1.o and indeed: nm --print-arma /home/andrea/.cabal/lib/mylib-0.1/ghc-6.10.1/HSmylib-0.1.o | grep my_var 0000001c D my_var So I desperately try: ghci /home/andrea/.cabal/lib/mylib-0.1/ghc-6.10.1/HSmylib-0.1.o -lmylib /tmp/ffi-test/bindings/test_lib.hs GHCi, version 6.10.1: http://www.haskell.org/ghc/ :? for help Loading object (static) /home/andrea/.cabal/lib/mylib-0.1/ghc-6.10.1/HSmylib-0.1.o ... done Loading object (dynamic) mylib ... failed. <command line>: user specified .o/.so/.DLL could not be loaded (/tmp/ffi-test/libmylib.so: undefined symbol: my_var) Whilst trying to load: (dynamic) mylib Additional directories searched: (none) Is this a bug? An intended behaviour? Is there a way out? What am I missing? Obviously the problem goes away if I link mylib.o with stub.o into libmylib.so.1.0. Thanks for your help. Andrea ps: here you can find a small shell script to automate the proposed test (included in the tarball linked above): http://gorgias.mine.nu/ffi-test/test_dynamic.sh

2 1

Three Recursively defined modules
by Chris Kuklewicz 09 Dec '08

09 Dec '08

Hi, As "hs-boot" is ghc specific method I am asking on this glasgow-haskell-users mailing list first. My hprotoc program converts message definitions into Haskell modules, and mimicking the expected OOP-like namespaces has been successful so far. It is possible to define messages and keys that create recursive modules dependencies, and I have left fixing this to the user. For the examples I have run across this has been possible to do manually. But I can easily write a file which generates three recursively defined modules with keys that I have not been able to fix with hs-boot files. I have created toy versions of the 3 modules and their "key"s which contain the problem. Can anyone see how to use hs-boot files to compile the three modules below? Note: The 3 modules ought to be the same aside from cyclic [a,b,c] replacement: > module A(A(..),akeybc,akeycb) where > > import B(B) > import B(bkeyac) > import C(C) > import C(ckeyab) > > data A = A { name :: String } > > akeybc :: Either B (Maybe C) > akeybc = Right Nothing > > akeycb :: Either C (Maybe B) > akeycb = Right Nothing > > instance Show A where > show a = concat [name a,show bkeyac,show ckeyab] > module B(B(..),bkeyca,bkeyac) where > > import A(A) > import A(akeybc) > import C(C) > import C(ckeyba) > > data B = B { name :: String } > > bkeyca :: Either C (Maybe A) > bkeyca = Right Nothing > > bkeyac :: Either A (Maybe C) > bkeyac = Right Nothing > > instance Show B where > show b = concat [name b,show ckeyba,show akeybc] > module C(C(..),ckeyab,ckeyba) where > > import A(A) > import A(akeycb) > import B(B) > import B(bkeyca) > > data C = C { name :: String } > > ckeyab :: Either A (Maybe B) > ckeyab = Right Nothing > > ckeyba :: Either B (Maybe A) > ckeyba = Right Nothing > > instance Show C where > show c = concat [name c,show akeycb,show bkeyca] It would be disappointing if I had to move the "key"s into separate modules/namespaces to allow for a solution using hs-boot files. Thanks, Chris

2 1

Type checker loops with type families, overlapping and undecidable instances
by José Pedro Magalhães 08 Dec '08

08 Dec '08

Hello all, Please consider the following code: {-# OPTIONS -Wall #-} > {-# LANGUAGE FlexibleContexts #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE OverlappingInstances #-} > {-# LANGUAGE UndecidableInstances #-} > > module Test where > > -- Some view > class Viewable a where > type View a > to :: a -> View a > > -- Structural representations > data Unit = Unit > data a :+: b = L a | R b > > instance Viewable Unit where > type View Unit = Unit > to = id > > instance (Viewable a, Viewable b) => Viewable (a :+: b) where > type View (a :+: b) = a :+: b > to = id > > -- Worker class > class F' a where > f' :: a -> () > > instance F' Unit where > f' Unit = () > > instance (F a, F b) => F' (a :+: b) where > f' (L x) = f x > f' (R x) = f x > > > -- Dispatcher class > class (Viewable a, F' (View a)) => F a where > f :: a -> () > f = f' . to > > instance F Unit where > f = f' > > instance (F a, F b) => F (a :+: b) where > f = f' > > -- All generic instances > instance (Viewable a, F' (View a)) => F a > > > -- A recursive datatype > data Nat = Zero | Succ Nat > > -- Instance of Viewable > instance Viewable Nat where > type View Nat = Unit :+: Nat > to = undefined > > -- Uncommenting the line below causes the typechecker to loop (GHC 6.10.1, > Windows) > --test = f Zero > Is this expected behavior or a bug? Thanks, Pedro

5 5

Re: Weak pointers and STM
by Simon Marlow 08 Dec '08

08 Dec '08

The way to use finalizers is in conjunction with an exception handler that provides an absolute guarantee that the resource will be reclaimed on exit. Note that Java doesn't guarantee to run finalizers on exit either: http://java.sun.com/j2se/1.4.2/docs/api/java/lang/Runtime.html#runFinalizer… Although in Java it's for different reasons. We can give more guarantees to C finalizers because they're much simpler: - a C finalizer can't synchronise with other Haskell code, including Haskell finalizers. - we don't have to worry about whether a C finalizer refers to other finalizable objects - we don't mind if a C finalizer blocks: that's the programmer's problem. Cheers, Simon Lennart Augustsson wrote: > From a theoretical perspective I'd say that they are completely > useless, because there's no guarantee that the finalizer will ever > run. You might as well throw them away as use them and there would be > the same guarantees. > From a practical perspective they are useful, because they probably > run. So you can use them to reclaim most resources. > > I realize that the situation is complicated in ghc, but it also means > that to get finalizers with guarantees you have to implement them > yourself rather than relying on the ghc runtime system, which can be > quite tedious. > > -- Lennart > > On Mon, Dec 8, 2008 at 9:59 AM, Simon Marlow <marlowsd(a)gmail.com> wrote: >> Lennart Augustsson wrote: >>> Finalizers without guarantees, like what ghc implements, are totally >>> useless. Since there is no guarantee that the finalizer will ever run >>> attaching one is a no-op. It has bitten me several times. I wish ghc >>> implemented finalizers according to the ffi spec. >> We do plan to do that (I'm sure you're aware of bug #1364), however I'm sure >> you're also aware that GHC's finalizers are more general than the FFI spec >> requires in that finalizers can be Haskell computations, and it is this that >> leads to the lack of guarantees. Implementing the FFI-style finalizers >> requires us to treat C finalizers as a special case, rather than >> implementing them as foreign calls from Haskell finalizers, which is a bit >> of a pain. >> >> I disagree that finalizers are completely useless. They're just not useful >> for some of the things you might like them to be useful for, like guaranteed >> resource reclamation. >> >>> -- Lennart (iPhone) >> Cheers, >> Simon (MS natural keyboard and 28" LCD screen) >> >>> On Dec 7, 2008, at 13:12, "Claus Reinke" <claus.reinke(a)talk21.com> wrote: >>> >>>>> Adding finalizers to arbitrary objects was useful for the memo table >>>>> application we had in mind when weak pointers were introduced, but for all >>>>> the other applications I've come across since then, we really want to add >>>>> finalizers to objects whose lifetimes are under programmer control. Notice >>>>> how ForeignPtrs attach the finalizer carefully to the MutVar# inside the >>>>> ForeignPtr, not the ForeignPtr itself. >>>> One application that was effectively killed by GHC's approach to >>>> finalizers was GHood (I lost interest when it became apparent that >>>> GHC was moving away from giving any kinds of guarantees about >>>> finalizers). The idea was that, just as unsafePerformIO gives us a >>>> way to instrument the evaluator, so finalizers could have given us a way >>>> to instrument garbage collection. Then GHood could not only >>>> have shown when which parts of which structure are first observed >>>> (how and when structures get unfolded) but also (roughly) when which >>>> parts of which structure become unreachable (how and when >>>> structures disappear again). That would have made a very nice tool. >>>> >>>> But it would have needed finalizers on arbitrary objects that are >>>> actually guaranteed to be run, preferably promptly, but not early. Given >>>> the application, I would have considered wrapping/annotating those objects >>>> in some transparent way, not visible to the original program, but forcing >>>> the memory manager to keep track of that object even if that means worse >>>> code. Only that there are no guarantees whatsoever on these finalizers >>>> anymore (there were some back then, but it emerged that they weren't backed >>>> up by the implementation). >>>> Which also hurts other, table-like, applications: I have an application >>>> where I need to keep track of synchronous communication channels, basically: >>>> advance each live channel at every step. Now, I would like to attach >>>> finalizers to the channels, so that when there are no more threads having >>>> references to a channel, the channel gets removed >>>> from the tracking table. But without finalizer guarantees, there is no >>>> guarantee that the table will not simply keep accumulating more and >>>> more of those dynamically created channels.. >>>> >>>> I, for one, would like to have good support for "adding finalizers to >>>> arbitrary objects with useful run guarantees". Actually, it is a bit hard >>>> to understand what finalizers without any guarantees (System.Mem.Weak) >>>> are supposed to achieve? >>>> >>>> Claus >>>> >>>> _______________________________________________ >>>> Glasgow-haskell-users mailing list >>>> Glasgow-haskell-users(a)haskell.org >>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>

2 1

Re: Weak pointers and STM
by Simon Marlow 08 Dec '08

08 Dec '08

Lennart Augustsson wrote: > Finalizers without guarantees, like what ghc implements, are totally > useless. Since there is no guarantee that the finalizer will ever run > attaching one is a no-op. It has bitten me several times. I wish ghc > implemented finalizers according to the ffi spec. We do plan to do that (I'm sure you're aware of bug #1364), however I'm sure you're also aware that GHC's finalizers are more general than the FFI spec requires in that finalizers can be Haskell computations, and it is this that leads to the lack of guarantees. Implementing the FFI-style finalizers requires us to treat C finalizers as a special case, rather than implementing them as foreign calls from Haskell finalizers, which is a bit of a pain. I disagree that finalizers are completely useless. They're just not useful for some of the things you might like them to be useful for, like guaranteed resource reclamation. > -- Lennart (iPhone) Cheers, Simon (MS natural keyboard and 28" LCD screen) > On Dec 7, 2008, at 13:12, "Claus Reinke" <claus.reinke(a)talk21.com> wrote: > >>> Adding finalizers to arbitrary objects was useful for the memo table >>> application we had in mind when weak pointers were introduced, but >>> for all the other applications I've come across since then, we really >>> want to add finalizers to objects whose lifetimes are under >>> programmer control. Notice how ForeignPtrs attach the finalizer >>> carefully to the MutVar# inside the ForeignPtr, not the ForeignPtr >>> itself. >> >> One application that was effectively killed by GHC's approach to >> finalizers was GHood (I lost interest when it became apparent that >> GHC was moving away from giving any kinds of guarantees about >> finalizers). The idea was that, just as unsafePerformIO gives us a >> way to instrument the evaluator, so finalizers could have given us a >> way to instrument garbage collection. Then GHood could not only >> have shown when which parts of which structure are first observed >> (how and when structures get unfolded) but also (roughly) when which >> parts of which structure become unreachable (how and when >> structures disappear again). That would have made a very nice tool. >> >> But it would have needed finalizers on arbitrary objects that are >> actually guaranteed to be run, preferably promptly, but not early. >> Given the application, I would have considered wrapping/annotating >> those objects in some transparent way, not visible to the original >> program, but forcing the memory manager to keep track of that object >> even if that means worse code. Only that there are no guarantees >> whatsoever on these finalizers anymore (there were some back then, but >> it emerged that they weren't backed up by the implementation). >> Which also hurts other, table-like, applications: I have an >> application where I need to keep track of synchronous communication >> channels, basically: advance each live channel at every step. Now, I >> would like to attach finalizers to the channels, so that when there >> are no more threads having references to a channel, the channel gets >> removed >> from the tracking table. But without finalizer guarantees, there is no >> guarantee that the table will not simply keep accumulating more and >> more of those dynamically created channels.. >> >> I, for one, would like to have good support for "adding finalizers to >> arbitrary objects with useful run guarantees". Actually, it is a bit hard >> to understand what finalizers without any guarantees (System.Mem.Weak) >> are supposed to achieve? >> >> Claus >> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users(a)haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

1 0

Weak pointers and STM
by John Meacham 07 Dec '08

07 Dec '08

Are there any caveats to using weak pointers and STM together? in particular, the two cases I am interested in are 1. is using 'deRefWeak' fully safe inside 'unsafeIOtoSTM'? As in, will it combine arbitrary STM actions with checking if a weak pointer is still valid atomically? 2. is using an atomically retry safe inside of a finalizer? Will it introduce any concurrency bottlenecks or can I just consider code run in a finalizer just like code run in any other thread? I just wanted to be sure before I base an integral component of a projects design on these working properly. thanks! John -- John Meacham - ⑆repetae.net⑆john⑈

4 6

Deriving Functor
by Twan van Laarhoven 07 Dec '08

07 Dec '08

Hello Ghc people, I have been working on adding support for "derive Functor" to ghc. I have a patch that mostly works, but there are some problems: 1. Ghc reports the correct instance when I use -ddump-deriv:, but that instance is not subsequenctly used. Instead I get a warning like: Warning: No explicit method nor default method for `fmap' In the instance declaration for `Functor (Cont r)' What could be going on here? The full output is attached. 2. As far as I understand the code, there would need to be three traversals of a data type T to derive an instance Functor T: - First to determine whether the deriving should be allowed at all (checkSideConditions) - Then to determine the constraints needed (mk_data_eqn) - Finally to make the body of the instance (gen_Functor_binds) This seems a bit redundant, and currently the code only does the last pass. It would make more sense to report any errors during this pass as well. I don't understand how the constraints are determined in TcDeriv, for instance for the type data T1 a b c = T1 a deriving (Eq) it seems as if Eq constraints are added for all of {a,b,c}, but somehow only a constraint Eq a ends up in the final instance. How does that work? The (experimental) patch was too large to attach, it can be found at http://twan.home.fmf.nl/files/deriv-functor-experimental1.patch.gz By the way: is there any advantage (besides readability) to generating the code "fmap f" instead of "\x -> fmap f x"? Twan E:\Dev\ghc\ghc-head3\testsuite\tests\ghc-regress\deriving\should_run>e:\dev\ghc\ghc-head3\ghc\stage1-inplace\ghc -c drvrun-functor2.hs -fforce-recomp -ddump-deriv ==================== Derived instances ==================== InstInfo: forall r_aff. GHC.Base.Functor (Main.Cont r_aff) { GHC.Base.fmap f_afU (Main.Cont a1_afW) = Main.Cont (\ b1_afY -> a1_afW (\ b2_ag0 -> b1_afY (f_afU b2_ag0))) } InstInfo: forall r_afj w_afk. GHC.Base.Functor (Main.ReaderWriter r_afj w_afk) { GHC.Base.fmap f_ag4 (Main.RW a1_ag6) = Main.RW (\ b1_ag8 -> case a1_ag6 b1_ag8 of { ((a1_aga, a2_agc)) -> (f_ag4 a1_aga, a2_agc) }) } drvrun-functor2.hs:8:14: Warning: No explicit method nor default method for `fmap' In the instance declaration for `Functor (ReaderWriter r w)' drvrun-functor2.hs:11:14: Warning: No explicit method nor default method for `fmap' In the instance declaration for `Functor (Cont r)'

1 0

hsc2hs problem
by Creighton Hogg 05 Dec '08

05 Dec '08

Hello, Since hsc2hs is distributed with GHC, I thought this might be a decent place to ask. I tried to run hsc2hs on a file that I know worked with my 6.8.3 installation, but now I'm getting the error /usr/local/lib/ghc-6.10.1/hsc2hs-0.67/template-hsc.h:4:19: error: HsFFI.h: No such file or directory Thanks, Creighton

2 4

Future kind system, closed type functions and type classes
by Philip K.F. Hölzenspies 05 Dec '08

05 Dec '08

Dear all, My apologies for the lengthy mail. There is a question at the end about whether all types in (of?) a kind closed under a type function can be concluded to be a member of a type class (i.e. whether kind classes are required for what I want to do). I have been trying to reserect Robert Dockins' TypeNats library [1], by pulling it out of the type classes / functional dependencies space and into the type family space. The current (discontinued) TypeNats has one Very Nice Thing to it; naturals are coded as bits, rather than as plain successors. Length annotations of vectors et al. now have a memory complexity of O(lg N) as opposed to O(N). A naïve implementation attempt runs into a rather obvious problem: data Z data I n data O n class Natural n where type Pred n toIntegral :: Integral i => n -> i toPred :: Natural n => n -> Pred n toPred _ = undefined instance Natural Z where type Pred Z = Z toIntegral _ = 0 instance Natural (I n) where type Pred (I n) = O n toIntegral n = let i = toIntegral (toPred n) in succ (i+i) instance Natural (O n) where type Pred (O n) = I (Pred n) toIntegral n = let i = toIntegral (toPred n) in i+i This should be interpreted as follows: Z denotes the empty bit string. I denotes a 1 and O denotes a 0. The bits are in reversed order, so 6 is coded as O(I(I Z)). One would expect the instance declaration of O to require a context "Natural n," because of "Pred n" and "toPred n," but the type checker allows for this. As a matter of fact, introducing the context "Natural n" to both the instance declarations of I and O raises the error: Could not deduce (Natural (Pred n)) from the context (Integral a) arising from a use of `natToIntegral' (in the instance declaration of O n) Leaving the context out, this implementation causes stack overflows when evaluating "toIntegral (undefined :: I Z)", because (O Z) is not reduced to Z. The FD solution is to introduce a class that describes the "canonical form" of a bit string (where the canonical form of O Z is Z): class Canonical n cfunctions for Haskell Tom Schrijv | n -> c Since we now have type functions, we can express this in a considerably more comprehensive manner. We can simply write: type family CanonicalNat c type family CanonicalNat_ c type instance CanonicalNat Z = Z type instance CanonicalNat (I n) = I (CanonicalNat n) type instance CanonicalNat (O n) = CanonicalNat_ (O (CanonicalNat n)) type instance CanonicalNat_ (O Z) = Z type instance CanonicalNat_ (O (O n)) = O (O n) type instance CanonicalNat_ (O (I n)) = O (I n) With the type function CanonicalNat, toPred can now be redefined to give a predecessor of a canonical type: toPred :: Natural n => n -> CanonicalNat (Pred n) toPred _ = undefined Unfortunately: Could not deduce (Natural (CanonicalNat_ (O (CanonicalNat n)))) from the context (Integral a) arising from a use of `natToIntegral' Adding a context to the definitions of I and O, viz. data Natural n => I n data Natural n => O n doesn't help very much. I'm no inference expert, but it seems that the problem is that inference goes up, not down (or vice versa, depending on how you interpret these words). Also, adding contexts to the results of type functions is a non-trivial thing [2]). In Schrijvers et al. [3], it is mentioned that work is being undertaken in the direction of closed type functions by using kind declarations. For this example, this would look something like: datakind NatNum = Z | I NatNum | O NatNum and type family CanonicalNat (c :: NatNum) :: NatNum Ideas for a new kind system for GHC is discussed on the wiki [4]. The interaction with type classes section shows this example (for Z/Succ represented Peano numbers): data kind Nat = Zero | Succ Nat class LessThanOrEqual (n1 :: Nat) (n2 :: Nat) instance LessThanOrEqual Zero Zero instance LessThanOrEqual n m => LessThanOrEqual n (Succ m) Aside from the fact that I would imagine that there is a missing case here instance LessThanOrEqual n m => LessThanOrEqual (Succ n) (Succ m) which is non-trivial because of the overlap with the second instance declaration, it is hard for me to see whether a checker with this new kind system could decide that all types in Nat have corresponding instances in LessThanOrEqual. It should be clear how this relates to my case described above; can it now be decided that the result of CanonicalNat will always have an instance of the Natural class? Regards, Philip PS. A possible purpose of a function such as toIntegral is to have a length implementation for fixed-length lists that is more lazy than the length function on a list, but that can be used in exactly the same way. [1] http://www.cs.princeton.edu/~rdockins/dist/typenats-0.2-source.tar.gz [2] http://content.ohsu.edu/cgi-bin/showfile.exe?CISOROOT=/etd&CISOPTR=227&file… [3] http://research.microsoft.com/~simonpj/papers/assoc-types/ifl2007.pdf [4] http://hackage.haskell.org/trac/ghc/wiki/KindSystem

1 0