Re: [Haskell-cafe] What puts False before True?
> > What is the basic philosophy for Bool being a member of Ord? > What justifies False < True? The implication ordering, which on this smallest non-trivial Boolean algebra happens to be a linear order, is therefore the natural candidate for Ord, the type class of ``default linear orders''. False ==> True Wolfram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The C Equiv of != in Haskell miscommunication thread
> > P.S. Have some cute code: > > Control.Monad.Fix.fix ((1:) . scanl (+) 1) Cute! But what an un-cute qualified name: :t Control.Monad.Fix.fix Control.Monad.Fix.fix :: (a -> a) -> a Has nothing to do with monads, and would perhaps be considered as ``out of Control'' in any case... ;-) Wolfram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
> > > * It would be nice if this worked inside the do-notation, too: > > > > do x :: Ordering > > x <- m > > > > (This is curently a syntax error.) > > I think the following works with -fglasgow-exts: > > do (x :: Ordering) <- m I know, but it is not as nice! ;-) Wolfram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Displaying infered type signature of 'offside' functions
Jules Bean <[EMAIL PROTECTED]> wrote,
concerning the problem of getting at the types of local definitions:
> Simon Peyton-Jones wrote:
> The principal difficulties here are to do with "what do we want"
> rather the implementation challenges.
>
> > 1. Should the compiler print the type of every declaration? Should GHCi
> > allow you to ask the type of a local decl?
> >
>
> IMO, ghci should definitely allow you to ask. This comes up for me every
> time that I write any haskell code (and in general I end up hoisting
> local definitions to the top level, which is a real pain if there is
> local scope, data or type, to hoist with it).
>
> > 2. How should the variables be identified? There may be many local
> > bindings for 'f', so you can't say just ":t f". Ditto if dumping all
> > local bindings.
> >
> >
>
> I think this is a hard question. I was imagining some kind of
> hierarchical system like foo.f, in the case that f is locally defined
> inside foo. (Yes I know we can't easily use '.' for that). There might
> be might be multiple fs inside the definition of foo; indeed there might
> even be multiple fs nested inside each other.
I just wanted to contribute a PRACTICAL TRICK I use:
* If the local definition is a pattern binding
f = ...
then I just add
f :: Ordering
* If the local definition is a, say binary, function binding
f p1 p2 = ...
then I just add
f :: Float -> Double -> Ordering
(Type does not matter for the number of function arrows you need to put;
only the syntactic arity of the bindings matters here.)
This relies on the fact that the types Float, Double, and Ordering
very rarely occur in my code --- pick your own.
Now the compiler gives you wonderful error messages
``cannot match type `x y z' against Ordering'' ---
so you replace ``Ordering'' with ``x y z''.
If there are type variables in ``x y z''
that come from the context,
take care that you have
{-# LANGUAGE ScopedTypeVariables #-}
at the beginning of your module
(after the {-# OPTIONS ...#-} line,
which should, as a matter of style,
NOT contain -fglasgow-exts
)
and the necessary ``forall ty1 ty2 ...'' in front of your the type
in the type signature of the enclosing definition.
At the cost of a re-compilation, this works wonderfully for me,
and is much less painful than hoisting AND exporting local definitions.
But even I still have some wishes open:
* It would be nice if this worked inside the do-notation, too:
do x :: Ordering
x <- m
(This is curently a syntax error.)
* It would be nice if {-# LANGUAGE ScopedTypeVariables #-}
brought in no other extensions,
and if GHC would recommend
the appropriate LANGUAGE pragmas instead of -fglasgow-exts
when it determines that the user might have wanted some extension.
(What is the right Language.Extension for GADTs?)
Wolfram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Recursion in Haskell
>
> For absorbing the functional style of programming (which is what you really
> should be working on at this point),
For functional style and the reasoning attitude associated with lazy
functional programming, the following book is a good introduction:
@Book{Bird-2000,
author = {Richard Bird},
title = {Introduction to Functional Programming using {Haskell}},
year = 2000,
publisher = {Prentice-Hall}
}
This is the second edition of:
@Book{Bird-Wadler-1988,
year = 1988,
title = {Introduction to Functional Programming},
publisher = {Prentice-Hall},
author = {Richard Bird and Phil Wadler}
}
Wolfram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] factorising to prime numbers
> > If you look at the definition of 'powers' you'll note it's infinite. So > there's no easy way to take the product of this list, if I don't know > how many items to take from it. So you need finite lists. > > -- how many of the prime p are in the unique factorisation > -- of the integer n? > f 0 _ = 0 > f n p | n `mod` p == 0 = 1 + f (n `div` p) p > | otherwise = 0 > > powers n = map (f n) primes Extremely high-level hint: Move from div to divMod (i.e., let f return a pair), and add List.unfoldr (or takeWhile) capacities to map. ;-) Wolfram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Space Leak Help
>
> > \begin{code}
> > catWithLen :: [a] -> (Int -> [a]) -> [a]
> > catWithLen xs f = h 0 xs
> > where
> > h k [] = f k
> > h k (x : xs) = case succ k of-- forcing evaluation
> > k' -> x : h k' xs
> > \end{code}
> >
>
> Thanks but this gives a different problem:
>
> [EMAIL PROTECTED]:~/sha1> ./allInOne 101 +RTS -hc -RTS
> [2845392438,1191608682,3124634993,2018558572,2630932637]
> [2224569924,473682542,3131984545,4182845925,3846598897]
> Stack space overflow: current size 8388608 bytes.
> Use `+RTS -Ksize' to increase it.
Does it still do that if you youse seq instead of case?
\begin{code}
catWithLen :: [a] -> (Int -> [a]) -> [a]
catWithLen xs f = h 0 xs
where
h k [] = f k
h k (x : xs) = let k' = succ k
in k' `seq` x : h k' xs
\end{code}
Wolfram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Space Leak Help
>
> I have re-written SHA1 so that is more idiomatically haskell and it is easy
> to
> see how it implements the specification. The only problem is I now have a
> space leak. I can see where the leak is but I'm less sure what to do about
> getting rid of it.
>
> Here's the offending function:
>
> pad :: [Word8] -> [Word8]
> pad xs =
>xs ++ [0x80] ++ ps ++ lb
>where
> l = length xs
> pl = (64-(l+9)) `mod` 64
> ps = replicate pl 0x00
> lb = i2osp 8 (8*l)
I would try something along the following lines (untested):
\begin{spec}
catWithLen xs f = xs ++ f (length xs)
\end{spec}
\begin{code}
catWithLen :: [a] -> (Int -> [a]) -> [a]
catWithLen xs f = h 0 xs
where
h k [] = f k
h k (x : xs) = case succ k of-- forcing evaluation
k' -> x : h k' xs
\end{code}
\begin{code}
pad :: [Word8] -> [Word8]
pad xs = catWithLen xs f
where
f l = 0x80 : ps lb
where
-- we know that |l = length xs|
pl = (64-(l+9)) `mod` 64
ps = funPow pl (0x00 :)
lb = i2osp 8 (8*l)
\end{code}
If you are lucky, then the replicate and the (++lb) in the original code
might be fused by the compiler as an instance of foldr-build
or something related --- check the optimised core code.
In my variant I changed this to rely on efficient function powering
instead:
\begin{spec}
funPow k f = foldr (.) id $ replicate k f
\end{spec}
\begin{code}
funPow :: Int -> (a -> a) -> (a -> a)
funPow n f = case compare n 0 of
LT -> error ("funPow: negative argument: " ++ show n)
EQ -> id
GT -> pow n f
where
pow m g = if m > 1
then let (m',r) = divMod m 2
g' = g . g
in if r == 0
then pow m' g'
else pow m' g' . g
else g
\end{code}
(You will probably also consider using Data.Bits
for (`mod` 64), (8*), and (`divMod` 2).
)
Wolfram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs: the plot thickens?
Hi Connor,
> A puzzle for you (and for me too). I just tried to translate an old
> Epigram favourite (which predates Epigram by some time) into GADT-speak.
> It went wrong. I had a feeling it might. I wonder how to fix it: I
> imagine it's possible to fix it, but that some cunning may be necessary.
> Here it is:
>
> Type-level Nat
>
> > data Z = Z
> > data S x = S x
>
> Finite sets: Fin Z is empty, Fin (S n) has one more element than Fin n
>
> > data Fin :: * -> * where
> > Fz :: Fin (S n)
> > Fs :: Fin n -> Fin (S n)
To me, this looks more like ordinal numbers than like general finite sets:
For each type-level natural number n, the set Fin n contains
all object-level natural numbers k < n,
where k = Fs^k Fz .
> The "thinning" function: thin i is the order-preserving embedding from
> Fin n to Fin (S n) which never returns i.
>
> > thin :: Fin (S n) -> Fin n -> Fin (S n)
> > thin Fz i = Fs i
> > thin (Fs i) Fz = Fz
> > thin (Fs i) (Fs j) = Fs (thin i j)
So ``thin Fz i'' is defined for i = undefined :: Fin Z.
If you don't want this kind of effect, you might consider to keep the empty
type away from your calculations:
> {-# OPTIONS -fglasgow-exts #-}
> data Z = Z
> data S x = S x
> data Fin :: * -> * where
> Fz :: Fin (S n)
> Fs :: Fin (S n) -> Fin (S (S n))
> thin :: Fin (S (S n)) -> Fin (S n) -> Fin (S (S n))
> thin Fz i = Fs i
> thin (Fs i) Fz = Fz
> thin (Fs i) (Fs j) = Fs (thin i j)
This gets me one line farther into thicken.
But what is possible now:
Add a lifting (or embedding) function:
> lift :: forall n . Fin n -> Fin (S n)
> lift Fz = Fz
> lift (Fs i) = Fs (lift i)
> thicken0 :: forall n . Fin n -> Fin n -> Maybe (Fin n)
> thicken0 Fz Fz = Nothing
> thicken0 Fz (Fs j) = Just (lift j)
> thicken0 (Fs i) Fz = Just Fz
> thicken0 (Fs i) (Fs j) = case (thicken0 i j) of
> Nothing -> Nothing
> Just k -> Just (Fs k)
I think that one ley to your trouble is the fact that there is,
as far as I can see, no direct way to define
a predicate determining whether an Fin (S n) element
is the largest of its type:
> isMax :: forall n . Fin (S n) -> Bool
> isMax = undefined
This would need a type case on Fz :: Fin (S Z) ---
I'd dig through Oleg's posts about type equality checking.
If you can make this possible, cou can also define
> unlift :: forall n . Fin (S n) -> Maybe (Fin n)
> unlift = undefined
and get your original thicken from that.
Wolfram
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Fwd: Re: [Haskell-cafe] Typeclasses and GADT [Was: Regular Expressions without GADTs]]
> > On 26 Oct 2005 10:11:25 -0400, [EMAIL PROTECTED] > <[EMAIL PROTECTED]> wrote: > > Tomasz Zielonka <[EMAIL PROTECTED]> wrote > > Wed, 26 Oct 2005 13:37:29 +0200: > > > > > > Speaking about casts, I was playing with using GADTs to create a > > > non-extensible version of Data.Typeable and Data.Dynamic. > > > I wonder if it's possible to write such a thing without GADTs (and > > > unsafeCoerce, which is used in Data.Dynamic, IIRC). > > > > It is possible to get even closer to Typeable by using > > the same interface --- which is sufficient for some applications. > > Hmmm... but you use unsafeCoerce, don't you? ;-) > > I might have been unclear about it - I didn't want to use unsafeCoerce. > With unsafeCoerce you can easily implement Typeable/Dynamic without > GADTs, don't you? The misunderstanding was entirely on my side: I had not seen the previous discussion, but only been forwarded your last message by Jacques. Now I finally subscribed to haskell-cafe, too... My concern was more with the interface than with the implementation. I need ``TI'' (your ``Type'') to make some other things possible that are not possible with Data.Typeable, but also have a bunch of things that do work with Data.Typeable. With -ddump-minimal-imports, I see that most of my files import only (Typeable*(), gcast) from Data.Typeable --- only a fraction actually use TypeRep or typeOf*. My main point was that this common interface can be implemented also with the GADT implementation of Typeable, so there is no need to rewrite code based on that common interface. A seondary point was the use of separate types at separate kinds, corresponding to the separate Typeable* classes at separate kinds. Since your Type and my TI are essentially the same, your nice technique for the cast can of course be transferred --- while your Wrapper* types have a custom flavour, I use general type combinators that are useful also in other settings. These are essentially just the standard combinatory logic combinators (with some Haskell influence ;-): newtype Ix =Ix newtype K x y =Kx newtype Sf g x =S(f x (g x)) newtype Flip f x y =Flip (f y x) newtype Bf g x =B(f (g x)) Unfortunately we do not have kind polymorphism, so we have to define variants for all the kind combinations we need. Naming these is a challenge --- I am still experimenting. (attached module TypeCombinators) The attached modules now don't use unsafeCoerce any more (thanks!), but still include all the higher-kinded material. Wolfram TI.lhs Description: Binary data Typeable.lhs Description: Binary data TypeCombinators.lhs Description: Binary data GCast.lhs Description: Binary data NatNum.lhs Description: Binary data ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Fwd: Re: [Haskell-cafe] Typeclasses and GADT [Was: Regular Expressions without GADTs]]
Tomasz Zielonka <[EMAIL PROTECTED]> wrote
Wed, 26 Oct 2005 13:37:29 +0200:
>
> Speaking about casts, I was playing with using GADTs to create a
> non-extensible version of Data.Typeable and Data.Dynamic.
> I wonder if it's possible to write such a thing without GADTs (and
> unsafeCoerce, which is used in Data.Dynamic, IIRC).
It is possible to get even closer to Typeable by using
the same interface --- which is sufficient for some applications.
Otherwise, what I did recently is essentially equivalent
to the ``non-Dynamic part'' of Tomasz code
(and adding Dyn would of course work in the same way):
Thomasz' --> attached modules
---
data Type --> data TI.TI*
class Typed--> class Typeable.Typeable*
newtype Wrapper* --> replaced by the ``*''s above ;-)
Wolfram
--[[application/octet-stream
Content-Disposition: attachment; filename="TI.lhs"][quoted-printable]]
%include lhs2TeX.fmt
%include WKlhs.sty
\section{Type Indices}
%{-# OPTIONS_GHC -fglasgow-exts #-} taken out for lhs2tex
\begin{code}
module TI where
import NatNum
\end{code}
For each ground type |a| constructed only from supported type constructors,
there is exactly one \emph{type index} in |TI a|.
In that respect,
an element of |TI a|
is similar to the satisfaction of the constraint |Typeable a|.
The important difference between |TI a| and |Typeable a|
is that structural induction over the structure of a type
documented by a |TI a| contains references to the constituent types
\emph{at the type level},
while structural induction over |TypeRep| representations of
type structure made accessible by |Typeable a|
has no connection to the type level at all.
\begin{code}
data TI :: * -> * where
Triv :: TI ()
Bool :: TI Bool
Char :: TI Char
Nat :: TI Nat
Int :: TI Int
Integer :: TI Integer
Float :: TI Float
Double :: TI Double
Apply_0 :: TI_0 t -> TI a -> TI (t a)
Apply_1 :: TI_1 t -> TI_0 a -> TI (t a)
\end{code}
Since one of the limitations of |Data.Typeable|
is its naming scheme that does not accommodate higher-kinded type constructors,
we use a naming scheme that is at least somewhat open in that direction,
and provide
alternative names following the scheme of |Data.Typeable| as type synonyms.
\begin{code}
type TI1 = TI_0
type TI2 = TI_0_0
type TI3 = TI_0_0_0
\end{code}
\begin{code}
data TI_0 :: (* -> *) -> * where
Maybe :: TI_0 Maybe
List :: TI_0 []
Apply_0_0 :: TI_0_0 t -> TI a -> TI_0 (t a)
\end{code}
\begin{code}
data TI_0_0 :: (* -> * -> *) -> * where
Either :: TI_0_0 Either
Pair :: TI_0_0 (,)
Fct :: TI_0_0 (->)
Apply_0_0_0 :: TI_0_0_0 t -> TI a -> TI_0_0 (t a)
\end{code}
\begin{code}
data TI_0_0_0 :: (* -> * -> * -> *) -> * where
Tup3 :: TI_0_0_0 (,,)
\end{code}
Just to demonstrate a higher-order kind in this context,
we define the datatype recursion type constructor.
\begin{code}
data TI_1 :: ((* -> *) -> *) -> * where
Fix :: TI_1 DFix
data DFix f = DFix (f (DFix f))
\end{code}
Defining type index equality without requiring identical types
makes the implementation of the cast functions much easier.
\begin{code}
eqTI :: TI a -> TI b -> Bool
eqTI Triv Triv = True
eqTI Bool Bool = True
eqTI Char Char = True
eqTI Nat Nat = True
eqTI Int Int = True
eqTI Integer Integer = True
eqTI Float Float = True
eqTI Double Double = True
eqTI (Apply_0 t a) (Apply_0 t' a') = eqTI_0 t t' && eqTI a a'
eqTI (Apply_1 t a) (Apply_1 t' a') = eqTI_1 t t' && eqTI_0 a a'
eqTI _ _ = False
\end{code}
\begin{code}
eqTI_0 :: TI_0 t -> TI_0 t' -> Bool
eqTI_0 Maybe Maybe = True
eqTI_0 List List = True
eqTI_0 (Apply_0_0 t a) (Apply_0_0 t' a') = eqTI_0_0 t t' && eqTI a a'
eqTI_0 _ _ = False
\end{code}
\begin{code}
eqTI_1 :: TI_1 t -> TI_1 t' -> Bool
eqTI_1 Fix Fix = True
eqTI_1 _ _ = False
\end{code}
\begin{code}
eqTI_0_0 :: TI_0_0 t -> TI_0_0 t' -> Bool
eqTI_0_0 Either Either = True
eqTI_0_0 Pair Pair = True
eqTI_0_0 Fct Fct = True
eqTI_0_0 _ _ = False
\end{code}
%{{{ EMACS lv
% Local Variables:
% folded-file: t
% fold-internal-margins: 0
% eval: (fold-set-marks "%{{{ " "%}}}")
% eval: (fold-whole-buffer)
% end:
%}}}
--[[application/octet-stream
Content-Disposition: attachment; filename="Typeable.lhs"][quoted-printable]]
%include lhs2TeX.fmt
%include WKlhs.sty
\section{Home-made |Typeable|}
%{-# OPTIONS_GHC -fglasgow-exts #-} taken out for lhs2tex
\begin{code}
module Typeable where
import NatNum
import TI
import GHC.Base ( unsafeCoerce# )
\end{code}
This module is currently happily restricting itself to Glasgow Haskell.
Many things that are done in a more portable way in |Data.Typeable|
are done in a more concise, but GHC-specific way here.
The following function is GHC-specific:
\begin{code}
unsafeCoerce :: a -> b
unsafeCoerce = unsafeCoerce#
\end{code}
For the tyme being, we only go to |Typeable3|,
while |Data.Typeable| goes all the way to |Typeable7|.
\begin{code}
class Typeable a where t
Re: Another space leak question
"Srineet" <[EMAIL PROTECTED]> writes: > Now [main2] continues forever, but doesn't cause hugs to run out of > heap.What' the reason that, while both [main1] and [main2] run forever, the > first causes hugs to run out of heap while second doesn't. referring to the following program (slightly adapted for compatibility with HOPS/MHA): > step1 :: [Int] -> Int -> Int > step1 (x:xs) n = step1 xs (n+x) > main1 :: Int > main1 = step1 (repeat 1) 1 > step2 :: [Int] -> Int -> Int > step2 (x:xs) n | n == 0= 0 >| otherwise = step2 xs (n+x) > main2 :: Int > main2 = step2 (repeat 1) 1 The reason is that the addition in step1 is deferred lazily, since its result is never needed. Therefore, unreduced additions accumulate. In contrast, the result of the addition in step2 is needed for comparison in ``n == 0'' --- this forces evaluation of n. I have produced two animations (hold down the space bar in ghostview to get the effect ;-), available at: http://ist.unibw-muenchen.de/kahl/MHA/Srineet_main1.ps.gz http://ist.unibw-muenchen.de/kahl/MHA/Srineet_main2.ps.gz A remedy might be to force sequentialisation: > step1' (x:xs) n = let n' = n+x in n' `seq` step1 xs n' Hope that helps! Wolfram http://ist.unibw-muenchen.de/kahl/ http://ist.unibw-muenchen.de/kahl/HOPS/ ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Why is there a space leak here?
David Bakin <[EMAIL PROTECTED]> writes: > Which of the various tools built-in or added to Hugs, GHC, NHC, etc. would > help me visualize what's actually going on here? I think Hood would (using > a newer Hugs, of course, I'm going to try it). What else? I just used my old ghc-4.06 add-in ``middle-end'' ``MHA'' to generate a HOPS module from David's message (slightly massaged, appended below), and then used HOPS to generate two animations: http://ist.unibw-muenchen.de/kahl/MHA/Bakin_foo1_20.ps.gz http://ist.unibw-muenchen.de/kahl/MHA/Bakin_foo2_20.ps.gz Hold down the space key in ghostview to get the animation effect! The left ``fan'', present in both examples, is the result list, and only takes up space in reality as long as it is used. The right ``fan'', visible only in foo1, contains the cycle of the definition of v, and represents the space leak. The take copies cons node away from the cycle. The HOPS input was generated automatically by an unreleased GHC ``middle end'' that is still stuck at ghc-4.06. The homepage of my term graph programming system HOPS is: http://ist.unibw-muenchen.de/kahl/HOPS/ Wolfram > module Bakin where -- This has a space leak, e.g., when reducing (length (foo1 100)) > foo1 :: Int -> [Int] > foo1 m > = take m v > where > v = 1 : flatten (map triple v) > triple x = [x,x,x] -- This has no space leak, e.g., when reducing (length (foo2 100)) > foo2 :: Int -> [Int] > foo2 m > = take m v > where > v = 1 : flatten (map single v) > single x = [x] -- flatten a list-of-lists > flatten :: [[a]] -> [a] > flatten [] = [] > flatten ([]:xxs) = flatten xxs > flatten ((x':xs'):xxs) = x' : flatten' xs' xxs > flatten' [] xxs= flatten xxs > flatten' (x':xs') xxs = x': flatten' xs' xxs ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
