Re: [Haskell-cafe] Joy Combinators (Occurs check: infinite type)
Keean Schupke wrote: > I have refactored your code into a type level Haskell program. > This has the nice advantage that it is extensible. Wow. Color me impressed. A little under a week ago, I stumbled onto Joy, and thought to myself that it could be translated almost directly into Haskell (which would imply it was possible to statically type). Well, it wasn't quite as direct as I had initially thought, but it looks like you've done it. Are there any papers/books out there which I could study to learn more about these (and other) tricks of the type system wizards? Thanks, Greg Buchholz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Joy Combinators (Occurs check: infinite type)
Greg Buchholz wrote: Keean Schupke wrote: Haskell is not dependantly typed, so cannot deal with types that "depend" on values. Can anyone recommend a nice dependently typed language to play with? Cayenne, Epigram, other? I have refactored your code into a type level Haskell program. This has the nice advantage that it is extensible. You can add a new primitive to the language as: data PrimName primName :: PrimName primName = undefined instance Apply PrimName a b where apply _ a = {- method implementing primName -} Programs are assembled as types like: fac4 = lit nul `o` lit suc `o` lit (dup `o` pre) `o` lit mult `o` linrec Recursion requires a primitive to aviod infinite types, see definitions of times, linrec and genrec. programs are run by applying the contructed type representing the program to a stack... for example: putStrLn $ show $ apply (lit hThree `o` fac4) hNil We could have written this: putStrLn $ show $ apply fac4 (hCons hThree hNil) I have attached the debugged code, simply load into ghci, in the same directory as the HList library (download http://www.cwi.nl/~ralf/HList) as Joy.hs. ghci -fallow-overlapping-instances Joy.hs (you need the flag to get the code to run interactively, however you dont need the flag just to run 'main' to perform the factorial tests) Keean. {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} module Joy where import MainGhcGeneric1 type HOne = HSucc HZero hOne :: HOne hOne = undefined type HTwo = HSucc HOne hTwo :: HTwo hTwo = undefined type HThree = HSucc HTwo hThree :: HThree hThree = undefined data Lit a lit :: a -> Lit a lit = undefined unl :: Lit a -> a unl = undefined instance HList s => Apply (Lit a) s (HCons a s) where apply a s = hCons (unl a) s class (HBool b,HList s) => HIfte b t f s s' | b t f s -> s' where hIfte :: b -> t -> f -> s -> s' instance (HList s,Apply t s s') => HIfte HTrue t f s s' where hIfte _ t _ s = apply t s instance (HList s,Apply f s s') => HIfte HFalse t f s s' where hIfte _ _ f s = apply f s data Ifte ifte :: Ifte ifte = undefined instance (Apply b s r,HHead r b',HIfte b' t f s s') => Apply Ifte (HCons f (HCons t (HCons b s))) s' where apply _ (HCons f (HCons t (HCons b s))) = hIfte (hHead (apply b s :: r) :: b') t f s data Nul nul :: Nul nul = undefined instance HList s => Apply Nul (HCons HZero s) (HCons HTrue s) where apply _ (HCons _ s) = hCons hTrue s instance HList s => Apply Nul (HCons (HSucc n) s) (HCons HFalse s) where apply _ (HCons _ s) = hCons hFalse s data EQ eq :: EQ eq = undefined instance (HList s,TypeEq a b t) => Apply EQ (HCons a (HCons b s)) (HCons t s) where apply _ (HCons a (HCons b s)) = hCons (typeEq a b) s data Dip dip :: Dip dip = undefined instance (HList s,HList s',Apply a s s') => Apply Dip (HCons a (HCons b s)) (HCons b s') where apply _ (HCons a (HCons b s)) = hCons b (apply a s) data Dup dup :: Dup dup = undefined instance HList s => Apply Dup (HCons a s) (HCons a (HCons a s)) where apply _ s@(HCons a _) = hCons a s data Pop pop :: Pop pop = undefined instance HList s => Apply Pop (HCons a s) s where apply _ (HCons _ s) = s data Swap swap :: Swap swap = undefined instance HList s => Apply Swap (HCons a (HCons b s)) (HCons b (HCons a s)) where apply _ (HCons a (HCons b s)) = hCons b (hCons a s) data Suc suc :: Suc suc = undefined instance (HNat a,HList s) => Apply Suc (HCons a s) (HCons (HSucc a) s) where apply _ (HCons _ s) = hCons (undefined::HSucc a) s data Pre pre :: Pre pre = undefined instance (HNat a,HList s) => Apply Pre (HCons (HSucc a) s) (HCons a s) where apply _ (HCons _ s) = hCons (undefined::a) s data Add add :: Add add = undefined instance (HList s,HAdd a b c) => Apply Add (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = hCons (hAdd (undefined::a) (undefined::b)) s class (HNat a,HNat b) => HAdd a b c | a b -> c where hAdd :: a -> b -> c instance HAdd HZero HZero HZero where hAdd _ _ = hZero instance HNat b => HAdd HZero (HSucc b) (HSucc b) where hAdd _ b = b instance HNat a => HAdd (HSucc a) HZero (HSucc a) where hAdd a _ = a instance (HNat (HSucc a),HNat (HSucc b),HNat c,HAdd a b c) => HAdd (HSucc a) (HSucc b) (HSucc (HSucc c)) where hAdd _ _ = hSucc $ hSucc $ hAdd (undefined::a) (undefined::b) data Sub sub :: Sub sub = undefined instance (HList s,HSub a b c) => Apply Sub (HCons b (HCons a s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = hCons (hSub (undefined::a) (undefined::b)) s class (HNat a,HNat b) => HSub a b c | a b -> c where hSub :: a -> b -> c instance HSub HZero HZero HZero where hSub _ _ = hZero instance HNat a => HSub (HSucc a) HZero (HSucc a) where hSub a _ = a instance HNat a => HSub HZero (HSucc a) HZero where hSub _ _ = hZero instance (HSub a b c) => HSub (HSucc a) (HSucc b) c where hSub _ _ = hSub (undefined::a) (undefined::b) data Mult mult :: Mult mult = undefined instance (HList s,HMul
Re: [Haskell-cafe] Joy Combinators (Occurs check: infinite type)
> Greg Buchholz wrote (on Wed, 09 Mar 2005 at 20:08): > Can anyone recommend a nice dependently typed language to play with? > Cayenne, Epigram, other? http://www.cs.chalmers.se/~catarina/agda/ See also the sexy IDE alfa: http://www.cs.chalmers.se/~hallgren/Alfa/ Peter Hancock ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Joy Combinators (Occurs check: infinite type)
Keean Schupke wrote: > Haskell is not dependantly typed, so cannot deal with types that "depend" on > values. Can anyone recommend a nice dependently typed language to play with? Cayenne, Epigram, other? Greg Buchholz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Joy Combinators (Occurs check: infinite type)
Greg Buchholz wrote: Keean Schupke wrote: I dont see why this is illegal... what do we want? take the top two items from the stack? With the code below (direct translation from tuples to HLists) I still get an occurs check error when trying to define fact5... Okay the reason is that types in the code end up depending on values. The type of the stack changes when items are pushed or popped. So the type of the stack returned from recursive functions depends on the recursion count... Haskell is not dependantly typed, so cannot deal with types that "depend" on values. This is why your code with tuples, and the HList code (which is really doing the same thing through a defined API) both fall down on the recursion. One solution is to make all elements the same type and use lists... like: data Elem = ElemInt Int | ElemChar Char... But this looses any static type checking. The alternative is to lift the "values" to the type level, using something like Peano numbers to represent naturals: data HZero = HZero data HSucc x = HSucc x Now different values have explictly different types, so we can have types which depend on them... Attached is an example implementation of "times" using this technique and the HList library (its not debugged... so there might be some mistakes). Keean. {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} module Joy where import MainGhcGeneric1 data Lit a = Lit a instance Apply (Lit a) s (HCons a s) where apply (Lit a) s = HCons a s data If = If instance Apply t s s' => Apply If (HCons f (HCons t (HCons HTrue s))) s' where apply _ (HCons _ (HCons t (HCons _ s))) = apply t s instance Apply f s s' => Apply If (HCons f (HCons t (HCons HFalse s))) s' where apply _ (HCons f (HCons _ (HCons _ s))) = apply f s data Eq = Eq instance TypeEq a b t => Apply Eq (HCons a (HCons b s)) (HCons t s) where apply _ (HCons a (HCons b s)) = HCons (typeEq a b) s data Dip = Dip instance Apply a s s' => Apply Dip (HCons a (HCons b s)) (HCons b s') where apply _ (HCons a (HCons b s)) = HCons b (apply a s) data Dup = Dup instance Apply Dup (HCons a s) (HCons a (HCons a s)) where apply _ s@(HCons a _) = HCons a s data Pop = Pop instance Apply Pop (HCons a s) s where apply _ (HCons _ s) = s data Swap = Swap instance Apply Swap (HCons a (HCons b s)) (HCons b (HCons a s)) where apply _ (HCons a (HCons b s)) = HCons b (HCons a s) class (HNat a,HNat b) => HAdd a b c | a -> b -> c where hadd :: a -> b -> c instance HAdd HZero HZero HZero where hadd _ _ = hZero instance HAdd HZero (HSucc b) (HSucc b) where hadd _ b = b instance HAdd a b c => HAdd (HSucc a) (HSucc b) (HSucc (HSucc c)) hadd _ _ = hadd (undefined::a) (undefined::b) data Add = Add instance HAdd a b c => Apply Add (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = HCons (hadd (undefined::a) (undefined::b)) s data Mult = Mult instance HMult a b c => Apply Mult (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = HCons (hadd (undefined::a) (undefined::b)) s data a @ b = a @ b instance (Apply a s s',Apply b s' s'') => Apply (a @ b) s'' where apply (O a b) s = apply b (apply a s :: s') type Square = Dup @ Mult type Cube = Dup @ Dup @ Mult data I = I instance Apply a s s' => Apply I (HCons a s) s' where apply _ (HCons a s) = apply a s data Times = Times instance Apply Times (HCons p (HCons HZero s)) s where apply _ (HCons _ s) = s instance Apply p s s' => Apply Times (HCons p (HCons (HSucc n) s) (HCons p (HCons n s')) where apply _ (HCons p (HCons _ s)) = HCons p (HCons (undefined::n) (apply p s)) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Parity of the number of inversions of a permutation
I think it is a quite popular problem. I have a permutation and I want to count how often a big number is left from a smaller one. More precisely I'm interested in whether this number is even or odd. That's for instance the criterion to decide whether Lloyd's shuffle puzzle is solvable or not. Example: 1 4 3 2 I can choose six pairs (respecting the order) of numbers out of it, namely (1,4) (1,3) (1,2) (4,3) (4,2) (3,2), where in the last three pairs the first member is greater than the second one. Thus I have 3 inversions and an odd parity. I' searching for a function which sorts the numbers and determines the parity of the number of inversions. I assume that there are elegant and fast algorithms for this problem (n * log n time steps), e.g. a merge sort algorithm. A brute force solution with quadratic time consumption is countInversions :: (Ord a) => [a] -> Int countInversions = sum . map (\(x:xs) -> length (filter (x>) xs)) . init . tails ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe