[Haskell-cafe] What does it mean to derive equations of restricted from in Haskell?
In John Hughes's The Design of Pretty printing library paper, he says: The implementations which we are trying to derive consist of equations of a restricted form. We will derive implementations by proving their constituent equations from the specification. By itself this is no guarantee that the implemented functions satisfy the specification because we might not have proved enough equation But if we also check that the derived definitions are terminating and exhaustive then this property is guaranteed What does restricted form mean? What is the meaning and significance of definitions are terminating and exhaustive? -- Daryoush Weblog: http://onfp.blogspot.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does it mean to derive equations of restricted from in Haskell?
Daryoush Mehrtash dmehrtash at gmail.com writes: What does restricted form mean? non-restricted: e.g., f (f x y) z = f x (f y z)) restricted: the shape of function declarations in Haskell (where lhs is a pattern) definitions are terminating ... non-termination: an equation like f x y = f y x when you orient it as a rule f x y - f y x, there are infinite derivations and exhaustive non-exhaustive: you have an equation f (x : ys) = ... but you don't have an equation for f [] = ... (all the above is is standard stuff in algebraic specification, equational reasoning, etc.) - J.W. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does the '~' mean ?
On Thu, Apr 15, 2010 at 10:59 PM, zaxis z_a...@163.com wrote: instance (BinaryDefer a, BinaryDefer b) = BinaryDefer (a,b) where put (a,b) = put2 a b get = get2 (,) size x = let ~(a,b) = x in size a + size b putFixed (a,b) = putFixed2 a b getFixed = getFixed2 (,) in `size` function, what does the `~` mean ? This is kind of a funny question, because in this case the ~ doesn't mean anything at all. Pattern matches in let are automatically irrefutable/lazy. A better way to write this is size ~(a,b) = size a + size b which is equivalent to size x = size a + size b where (a,b) = x which is equivalent to size x = let (a,b) = x in size a + size b which is equivalent to size x = let a = case x of (v,_) - v b = case x of (_,v) - v in size a + size b If a or b never get evaluated, the case statements (which will fail on bottom values) don't happen. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does the '~' mean ?
On 16 April 2010 15:59, zaxis z_a...@163.com wrote: instance (BinaryDefer a, BinaryDefer b) = BinaryDefer (a,b) where put (a,b) = put2 a b get = get2 (,) size x = let ~(a,b) = x in size a + size b putFixed (a,b) = putFixed2 a b getFixed = getFixed2 (,) in `size` function, what does the `~` mean ? A lazy pattern match: http://en.wikibooks.org/wiki/Haskell/Laziness (there is a better name for it, but I can't remember). -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does the '~' mean ?
Ivan, in `size` function, what does the `~` mean ? A lazy pattern match: http://en.wikibooks.org/wiki/Haskell/Laziness (there is a better name for it, but I can't remember). Irrefutable pattern? ;-) Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does the '~' mean ?
On 16/04/10 07:09, Ivan Miljenovic wrote: On 16 April 2010 15:59, zaxis z_a...@163.com wrote: instance (BinaryDefer a, BinaryDefer b) = BinaryDefer (a,b) where put (a,b) = put2 a b get = get2 (,) size x = let ~(a,b) = x in size a + size b putFixed (a,b) = putFixed2 a b getFixed = getFixed2 (,) in `size` function, what does the `~` mean ? A lazy pattern match: http://en.wikibooks.org/wiki/Haskell/Laziness (there is a better name for it, but I can't remember). Irrefutable patterns? /M -- Magnus Therning(OpenPGP: 0xAB4DFBA4) magnus＠therning．org Jabber: magnus＠therning．org http://therning.org/magnus identi.ca|twitter: magthe signature.asc Description: OpenPGP digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does the '~' mean ?
Stefan Holdermans ste...@vectorfabrics.com writes: Irrefutable pattern? ;-) Ahhh, yes, that's it. I knew it started with `i', but that's about it... -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] what does the '~' mean ?
instance (BinaryDefer a, BinaryDefer b) = BinaryDefer (a,b) where
put (a,b) = put2 a b
get = get2 (,)
size x = let ~(a,b) = x in size a + size b
putFixed (a,b) = putFixed2 a b
getFixed = getFixed2 (,)
in `size` function, what does the `~` mean ?
Sincerely!
-
fac n = let { f = foldr (*) 1 [1..n] } in f
--
View this message in context:
http://old.nabble.com/what-does-the-%27%7E%27-mean---tp28263383p28263383.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] What does it mean that objects are fixpoints? (OO'Haskell)
Hello! I'm trying to wrap my head around OO'Haskell's notion of objects as fixpoints. Is OO'Haskell's use of mfix simply a use of something like a monadic Y-combinator to give the object access to its own identity? Thanks, Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does it mean that objects are fixpoints? (OO'Haskell)
I'm trying to wrap my head around OO'Haskell's notion of objects as fixpoints. Is OO'Haskell's use of mfix simply a use of something like a monadic Y-combinator to give the object access to its own identity? I don't remember the details exactly, but isn't it to support open recursion for inherited/overridden methods? http://etymon.blogspot.com/2006/04/open-recursion-definition.html Regards, Sean ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What does it mean that objects are fixpoints? (OO'Haskell)
On Tue, Sep 15, 2009 at 10:14 AM, Manuel Simoni msim...@gmail.com wrote: Hello! I'm trying to wrap my head around OO'Haskell's notion of objects as fixpoints. Is OO'Haskell's use of mfix simply a use of something like a monadic Y-combinator to give the object access to its own identity? More or less, yes. To define 'self' or 'this'. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does atomically# mean?
I am having hard time making sense of GHC.Conc. Is there a writeup that describes the significance of #, or the meaning of primOp and primType? Thanks Daryoush On Sun, Dec 7, 2008 at 11:48 PM, Don Stewart d...@galois.com wrote: dmehrtash: Any idea was the atomically# mean in the following code? atomically :: STM a - IO a atomically (STM m) = IO (\s - (atomically# m) s ) Code is from GHC.Conc module [1] http://www.haskell.org/ghc/docs/6.6/html/libraries/base/GHC-Conc.html It is a primitive hook into the runtime, where transactional memory is implemented. It is documented in the primops module in the GHC source, $ cd ghc/compiler/prelude/ section STM-accessible Mutable Variables primtype TVar# s a primop AtomicallyOp atomically# GenPrimOp (State# RealWorld - (# State# RealWorld, a #) ) - State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True primop RetryOp retry# GenPrimOp State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True Along with other primitives like: section Parallelism primop ParOp par# GenPrimOp a - Int# with -- Note that Par is lazy to avoid that the sparked thing -- gets evaluted strictly, which it should *not* be has_side_effects = True -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does atomically# mean?
This might be of some help: http://www.haskell.org/ghc/docs/6.10.1/html/users_guide/syntax-extns.html Daryoush Mehrtash wrote: I am having hard time making sense of GHC.Conc. Is there a writeup that describes the significance of #, or the meaning of primOp and primType? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does atomically# mean?
That code is in ghc root/rts/STM.c -- ryan 2009/1/30 Daryoush Mehrtash dmehrt...@gmail.com: I like to look at the code where the runtime detects a TVar, inside an atomic block, has been changed by another thread and hence it aborts the atomic operation. Any suggestion as to where I would find the code? daryoush On Sun, Dec 7, 2008 at 10:48 PM, Don Stewart d...@galois.com wrote: dmehrtash: Any idea was the atomically# mean in the following code? atomically :: STM a - IO a atomically (STM m) = IO (\s - (atomically# m) s ) Code is from GHC.Conc module [1]http://www.haskell.org/ghc/docs/6.6/html/libraries/base/GHC-Conc.html It is a primitive hook into the runtime, where transactional memory is implemented. It is documented in the primops module in the GHC source, $ cd ghc/compiler/prelude/ section STM-accessible Mutable Variables primtype TVar# s a primop AtomicallyOp atomically# GenPrimOp (State# RealWorld - (# State# RealWorld, a #) ) - State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True primop RetryOp retry# GenPrimOp State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True Along with other primitives like: section Parallelism primop ParOp par# GenPrimOp a - Int# with -- Note that Par is lazy to avoid that the sparked thing -- gets evaluted strictly, which it should *not* be has_side_effects = True -- Don -- Daryoush Weblog: http://perlustration.blogspot.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does atomically# mean?
I like to look at the code where the runtime detects a TVar, inside an atomic block, has been changed by another thread and hence it aborts the atomic operation. Any suggestion as to where I would find the code? daryoush On Sun, Dec 7, 2008 at 10:48 PM, Don Stewart d...@galois.com wrote: dmehrtash: Any idea was the atomically# mean in the following code? atomically :: STM a - IO a atomically (STM m) = IO (\s - (atomically# m) s ) Code is from GHC.Conc module [1] http://www.haskell.org/ghc/docs/6.6/html/libraries/base/GHC-Conc.html It is a primitive hook into the runtime, where transactional memory is implemented. It is documented in the primops module in the GHC source, $ cd ghc/compiler/prelude/ section STM-accessible Mutable Variables primtype TVar# s a primop AtomicallyOp atomically# GenPrimOp (State# RealWorld - (# State# RealWorld, a #) ) - State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True primop RetryOp retry# GenPrimOp State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True Along with other primitives like: section Parallelism primop ParOp par# GenPrimOp a - Int# with -- Note that Par is lazy to avoid that the sparked thing -- gets evaluted strictly, which it should *not* be has_side_effects = True -- Don -- Daryoush Weblog: http://perlustration.blogspot.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] what does atomically# mean?
Any idea was the atomically# mean in the following code? atomically :: STM a - IO a atomically (STM m) = IO (\s - (*atomically# *m) s ) Code is from GHC.Conc module http://www.haskell.org/ghc/docs/6.6/html/libraries/base/GHC-Conc.html daryoush ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] what does atomically# mean?
dmehrtash: Any idea was the atomically# mean in the following code? atomically :: STM a - IO a atomically (STM m) = IO (\s - (atomically# m) s ) Code is from GHC.Conc module [1]http://www.haskell.org/ghc/docs/6.6/html/libraries/base/GHC-Conc.html It is a primitive hook into the runtime, where transactional memory is implemented. It is documented in the primops module in the GHC source, $ cd ghc/compiler/prelude/ section STM-accessible Mutable Variables primtype TVar# s a primop AtomicallyOp atomically# GenPrimOp (State# RealWorld - (# State# RealWorld, a #) ) - State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True primop RetryOp retry# GenPrimOp State# RealWorld - (# State# RealWorld, a #) with out_of_line = True has_side_effects = True Along with other primitives like: section Parallelism primop ParOp par# GenPrimOp a - Int# with -- Note that Par is lazy to avoid that the sparked thing -- gets evaluted strictly, which it should *not* be has_side_effects = True -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
