[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
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
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 (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)
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,HMult a b c) = Apply Mult (HCons a (HCons
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
