Re: type of minimumBy
"S.D.Mechveliani" wrote:
> (+), (&&) ... are different. Because they have classical tradition
> to be applied as binary infix operations.
> And gcd, min, max, lcm have not this "infix" tradition.
Yes, but the "infix tradition" is not the only reason we have these
operations. We have them because they are useful. They are the
simplest versions of the operations. If I want to sum up all the
elements of a binary tree, for example, I would use (+), not sum,
because I always want to add two numbers and I don't want the overhead
of intermediate lists. The same is true if I want the minimum element
of the tree.
I admit that, if the haskell compiler/interpreter inlines the list
versions, and implements list deforestation, then the list versions can
be just as efficient as the curried versions, but we can't always be
assured of this.
For economy of function names, and to avoid confusion between the
curried and list versions of operations, I would suggest an "L" suffix
for the list versions (not including sum, concat, etc.):
min:: (Ord a) => a -> a -> a
minL :: (Ord a) => [a] -> a
minBy :: (a -> a -> Ordering) -> a -> a -> a
minLBy :: (a -> a -> Ordering) -> [a] -> a
gcd:: (Integral a) -> a -> a -> a
gcdL :: {Integral a) -> [a] -> a
Best regards,
Matt Harden <[EMAIL PROTECTED]>
FRP/FRAN vs O'Haskell
Can someone give a brief comparison of the FRP approach with O'Haskell?
Both frameworks seem to revolve around asynchronous interaction between
objects in continuous time. The O'Haskell folks argue that you
need a new language to express this activity well. The FRP folk seem
happy with Haskell as is. FRAN handles events (e.g. mouseclicks). Is
there any reason it couldn't handle network events too?
Where does FRP fail such that a new language is required?
If the two systems are complimentary, how would FRP be enhanced by
O'Haskell?
-Alex-
___
S. Alexander Jacobson Shop.Com
1-212-697-0184 voiceThe Easiest Way To Shop (sm)
On Fri, 19 May 2000, Paul Hudak wrote:
> > Has anyone built any block simulators (for modeling continuous
> > electronic systems, like OP Amps, RC networks, etc) in Haskell?
>
> There have been several replies to this already, but permit me to add my
> 2 cents worth:
>
> FRP ("Functional Reactive Programming") is an abstraction of Fran
> ("Functional Reactive Animation") that is ideally suited to describing
> such things, since it is based on continuous (time-varying) values, as
> opposed to discrete values. You can find out a lot about Fran from
> Conal Elliott's home page (http://www.research.microsoft.com/~conal) and
> from my book (http://haskell.org/soe), and about FRP at
> http://haskell.org/frob. My student Zhongong Wan and I also have a new
> PLDI paper on the formal underpinnings of FRP if anyone is interested
> (it's not on the web yet).
>
> As for Haskore:
>
> > I'm also interested in this. I am thinking of extending
> > Paul Hudak's Haskore system to generate and handle true audio data
> > (instead of, or in addition to) MIDI data.
> >
> > I don't think I'll have enough time to do the programming myself,
> > but since I'll be using Hudak's book in next term's course,
> > I hope I can attract some students, and set them in the right
> > direction.
> >
> > In fact one student who read the course announcement
> > (and the book's web page) already asked me
> > about functional audio signal processing.
>
> The latest release of Haskore (http://haskell.org/haskore) includes an
> interface to Csound. That is, one can wire up oscillators, modulators,
> special effects, etc. in a nice declarative style in Haskell, which then
> gets compiled into a Csound instrument file, which in turn gets compiled
> by Csound into actual sound files (.wav, .snd, etc.). The nice thing
> about this is that it's fairly efficient because of the back-end
> processing. To do this in FRP would be much less efficient.
>
> Hope this helps,
>
> -Paul
>
Re: Block simulation / audio processing
> Am I correct in saying that the way time is handled is by a > function that gets the current time and functions that calculate > the state of the system at the time given by that call? So in FRP, > time is continuous, but the points of calculation are not controlled > by the Haskell code. I'm not sure I understand the question. Here's an example that might clarify. In FRP/Fran/Fal I can write "sin time". The meaning of that behavior depends on some kind of an interpreter. Normally, the intepreter tries to run it in real time, as I think you are suggesting, for example when trying to generate graphical animations. But you can define the interpeter any way that you like. For example, you could define one that took very small time steps, thus generating a very fine-grained animation that you played back later at a faster rate. Or you could define an interpreter mimicking the denotational semantics that would give you the single value of the behavior at some given point in time: sin time `at` pi/2 ==> 1 By the way, relative to a given interpreter, you can also do time transformations, such as: timeTrans (pi/2) (sin time) `at` 0 ==> 1 I hope this helps, -Paul
RE: Block simulation / audio processing
Paul,
I took a cursory look at your book. Am I correct in saying that the way time
is handled is by a function that gets the current time and functions that
calculate the state of the system at the time given by that call? So in FRP,
time is continuous, but the points of calculation are not controlled by the
Haskell code.
Mike
> -Original Message-
> From: Paul Hudak [mailto:[EMAIL PROTECTED]]
> Sent: Friday, May 19, 2000 6:45 AM
> To: [EMAIL PROTECTED]
> Cc: [EMAIL PROTECTED]
> Subject: Re: Block simulation / audio processing
>
>
> > Has anyone built any block simulators (for modeling continuous
> > electronic systems, like OP Amps, RC networks, etc) in Haskell?
>
> There have been several replies to this already, but permit
> me to add my
> 2 cents worth:
>
> FRP ("Functional Reactive Programming") is an abstraction of Fran
> ("Functional Reactive Animation") that is ideally suited to describing
> such things, since it is based on continuous (time-varying) values, as
> opposed to discrete values. You can find out a lot about Fran from
> Conal Elliott's home page
> (http://www.research.microsoft.com/~conal) and
> from my book (http://haskell.org/soe), and about FRP at
> http://haskell.org/frob. My student Zhongong Wan and I also
> have a new
> PLDI paper on the formal underpinnings of FRP if anyone is interested
> (it's not on the web yet).
>
> As for Haskore:
>
> > I'm also interested in this. I am thinking of extending
> > Paul Hudak's Haskore system to generate and handle true audio data
> > (instead of, or in addition to) MIDI data.
> >
> > I don't think I'll have enough time to do the programming myself,
> > but since I'll be using Hudak's book in next term's course,
> > I hope I can attract some students, and set them in the right
> > direction.
> >
> > In fact one student who read the course announcement
> > (and the book's web page) already asked me
> > about functional audio signal processing.
>
> The latest release of Haskore (http://haskell.org/haskore) includes an
> interface to Csound. That is, one can wire up oscillators,
> modulators,
> special effects, etc. in a nice declarative style in Haskell,
> which then
> gets compiled into a Csound instrument file, which in turn
> gets compiled
> by Csound into actual sound files (.wav, .snd, etc.). The nice thing
> about this is that it's fairly efficient because of the back-end
> processing. To do this in FRP would be much less efficient.
>
> Hope this helps,
>
> -Paul
>
Re: more detailed explanation about forall in Haskell
Fri, 19 May 2000 19:47:38 +0200, Iavor Diatchki <[EMAIL PROTECTED]> pisze: > i do not see the need for the "forall" quantifier to be written > explicitly however, It is needed when the quantifier is inside a function argument, to spell the difference between f1 :: forall a. ([a] -> [a]) -> [a] -> [a] and f2 :: (forall a. [a] -> [a]) -> [a] -> [a] the second being the same as f2 :: forall a. (forall b. [b] -> [b]) -> [a] -> [a] What is the difference? f1 cannot assume anything about "a". It only knows that the function passed as the first parameter can be applied to a value of the same type as the second parameter, yielding the same type, and that this type is a list of something. f2 can use its first parameter for any type "a" it chooses, even for different types in different places. For example to apply it to [False,False,True] and check if the first element of the result is True. When calling f1, we can pass it a function [Int]->[Int] and a list of Ints, or similarly for another type. OTOH as the first argument of f2 we must pass a polymorphic function that will accept any list, independently of the second argument. For example id, reverse, List.cycle, (take 5) and (\x -> x++x) are OK, but sort is not. I am generally talking about Haskell with GHC and Hugs extensions. Standard Haskell does not have explicit foralls, one cannot define a function like f2 in it, and one cannot write a type signature depending on type variables that are bound outside. forall is also used in local universal quantification and local existential quantification in data types - both are language extensions. I will not write about them here. > and i quite like the way haskell currently deals with the situation. Me too. Since in 99% of cases the quantifier is at the top of the signature, I like having it implicit in those cases, although it causes troubles (see below). Some people get confused, but IMHO they would get confused even when explicit forall was mandatory - the problem is in them, not in Haskell's syntax. > 3) f :: a f is of types 'a', where 'a' denotes some type This descripton looks unclear for me. I hope you meant that f can be used as a value of any type the caller chooses. So the caller can use f as a String. OTOH there is no much freedom in implementation of f, The only choice is bottom, and it can only be spelt differently: f = f f = undefined f = error "foo" They are theoretically the same, but in practice their effects are different. > 4) f :: a -> Int f is a function, which given an object of some type 'a' >returns an integer In other words, the caller can choose a type for "a" and use "f" as the type "a -> Int". This does not explain the intuitive meaning of "f" so well, but allows uniform understanding of all polymorphic types. > so my questions are: > > 1) what would it mean if one writes f :: a (in general: how does > one think of unbound type variables)? This type signature in program source means the same as "f :: forall a. a". Except two cases: - In a method signature inside class declaration, when "a" was in the class head. It means that f will have the type "forall a. Class a => a". - With GHC and Hugs extension of pattern type signatures, it means "f :: a" (for "a" bound outside) if "a" was indeed bound outside by a pattern type signature. Example: g :: b -> b -- The name "b" here is independent of all other names, g (x::a) = -- but the name "a" defined here can be used below: ... where f1 :: a -- The type of f1 is the same as of g's argument. -- It is not implicitly quantified by forall here! f2 :: b -- The type of f2 is forall b. b. -- This is the same type as forall z. z, etc. f3 :: forall a. a -- The type of f3 is the same as of f2. -- Thus forall can be used to be sure that we introduce -- a new type variable, and not mention one bound outside. When you use "f :: a" in an expression, not in a type signature among declarations, in GHC these rules apply too. In standard Haskell the second rule obviously does not apply, because there are no pattern type signatures, but the first does not apply either, which is not very obvious (one has a chance to write such expression in the default implementation of a method). In Hugs these rules don't apply for types in expressions, but maybe they will, I don't know. > 2) how will one write constraints on the types (e.g. as in > (7) above)? i presume that since with the 'forall' we get the > whole scoping thing, so the constraints have to be written per > quantifier, i.e. something like: > > f:: forall a of_class Eq. (a -> Int) No. The context is always written just inside forall, no matter if forall is explicit or not: f :: forall a. Eq a => a -> Int Similarly for local quantification: g :: Ord b => (forall a. Eq a => [a] -> [a]) -> [b] -> [b] It does not make sense to write context togeth
Re: more detailed explanation about forall in Haskell
>From: Peter Douglass <[EMAIL PROTECTED]> >To: 'Jan Brosius' <[EMAIL PROTECTED]>; Frank Atanassow <[EMAIL PROTECTED]> >Cc: <[EMAIL PROTECTED]> >Sent: Friday, May 19, 2000 6:03 PM >Subject: RE: more detailed explanation about forall in Haskell | Jan Brosius wrote: | | > look at this example: | > | > alpha(x) == x is_an Integer => x^2 > -1 | > | > this is an example of a formula that is true | > Sorry, this is not my logic. Since this formula is "true" it is allowed to be generalized forall x . alpha(x) == forall x. (x is_an Integer => x^2 > -1) and this may be rewritten in a more known form forall x. alpha(x) == [forall x is_an Integer. (x^2 > -1)] or still another way forall x. alpha(x) == [forall x `element_of` N) .( x^2 > -1)] (where N denotes the set of integers) which can be read as " forall x element of the set of integers N , x^2 > -1 " The forall in the above expression is an example of a bounded forall. It is also an example of a so called closed formula (because having no free variables anymore ) or also called a sentence. An other example , let R be the set of real numbers and we want to express that the square of a real number is always >= 0 then on can write beta == [forall x `element_of R . ( x^2 >= 0)] then by definition of a bounded forall : beta == [forall x . (x `element_of R => x^2 >= 0 )] and define next : alpha (x) ==( x `element_of R => X^2 >=0 ) Next remember that everybody agreed that the following is a TRUE implication: (*) forall x . alpha(x) => alpha(x) Finally remember that the Modus Ponens rule gives us a way to derive new theorems from implications : P => Q true Ptrue *** Q true Then I get [forall x . alpha(x)] => alpha(x) (true) forall x . alpha(x) (true) *** alpha(x) (true) So we get the true formula alpha(x) where x is free. I only wanted to state that this is not my logic and that IF one accepts the validity of the Modus Ponens rule and the fact agreed by everybody that the implication [forall x . alpha(x)] => alpha(x) is true, then one HAS to accept that the following formula alpha(x) is true. Finally, since I have been attacked by someone to have misread Bourbaki's book , well here you have something: Book entitled : " N. Bourbaki Elements de Mathematique editor : Hermann, Paris 1970 page: E I.39 Theoreme 1. - x = x " Designons par S la relation x = x de T0. .. For those who don't know French : In Bourbaki one proves theorem 1 : x = x this shows that alpha(x) == x = x is a true formula in a quantified theory with an equal sign A message to the one who liked to ridiculize me so much : If you don't agree with all this , please send your comments directly to Bourbaki (a famous french society of mathematicians ) , say to these mathematicians they are a laughing stock for all logicians from the time of Tarski , Gentzen and ... your name . Please don't forget to put a stamp on the envelope ( joke about Dutch). I hope that this will settle once and for all that this is not my logic , but I appreciate it much that you (the person in Dutch - land) want to give me full credit of their work. | > *If you want to come up with your own logic, where alpha(x) | > is equivalent to | > *forall x. alpha(x), then that's fine. | > | > No, if alpha(x) is a true formula then forall x. alpha(x) is | > again a true assertion | | I think part of the confusion here has to do with the notation alpha(x). | The traditional mathematical notation f(x) is ambiguous. It may either | refer to an abstraction or an application. In this regard, lambda notation | is much superior. What does the alpha(x) here mean? | If we assume it is a function like: | alpha = \ x . (x is_an Integer => x^2 > -1 ) | then it is meaningful to debate whether or not the inner 'x's refer to the | same x as the lambda bound x or whether "x is_an integer" creates a new | binding. | On the other hand, if we assume that alpha(x) is an application of alpha | to x then the debate seems to be whether x refers to some value, or whether | it is simply a place-holder. | Perhaps Jan can clarify what is meant here. | --Peter Douglass | | | | Still friendly greetings Jan Brosius
Re: more detailed explanation about forall in Haskell
hello, i have been following the evolution of haskell for about 2 years now in my spare time, but haven't had time to really get into haskell programming. so i am not an expert or anything. i do not see the need for the "forall" quantifier to be written explicitly however, and i quite like the way haskell currently deals with the situation. here is how i think about functions and their types. i would be glad if someone points out any mistakes i made, as (as i wrote above) i am by no means an advanced haskell user and am still learning. anyways here we go: 1) f :: Int f is of type integer 2) f :: Int -> Int f is a function, which given an integer produces and integer 3) f :: a f is of types 'a', where 'a' denotes some type (since we haven't imposed any restrictions on 'a' it can be any type, so the implicit universal quantification done by haskell makes sense) (would bottom be of this type?) 4) f :: a -> Intf is a function, which given an object of some type 'a' returns an integer (i.e. f does not assume anything about what its parameter might be, so f works on paramters of any type) 5) f :: a -> a f is a function, which given an object of some type 'a' returns an object of the *same* type 'a' 9again no restrictions on what 'a' might be) 6) f :: (Eq a) => a f is of type 'a', but 'a' is of class Eq, so now we have imposed some restrictions on the types of which f can be, i.e. any type, which can deal with equality 7) f :: (Eq a) => a -> Int is a function, which assumes that its parameter can deal with equality (so the function can compare the parameter to things for equality). however it does not assume anything else about its parameter. etc... so my questions are: 1) what would it mean if one writes f :: a (in general: how does one think of unbound type variables)? this is i think what the big discussion was all about, here are the solutions i can see: 1.1 this is an ivalid expressions, but then we get a more verbose version of what we have at the moment, is it worthed? 1.2 it is a valid expression and is the same as f :: forall a.a , i.e. it is implicitly universally quantified by haskell, so f :: forall a.a and f :: a is really the same thing. the probelm with this is that there is more than one way to write the same thing and will probably confuse the issue even more. 1.3 it is a valid expression, but has some other meaning, but what? 1.4 f is a type variable :-) . i just tought of this now, and i think this *really* will confuse things 2) how will one write constraints on the types (e.g. as in (7) above)? i presume that since with the 'forall' we get the whole scoping thing, so the constraints have to be written per quantifier, i.e. something like: f :: forall a of_class Eq. (a -> Int) but what about: f :: forall a of_class Eq. forall a.a now i think f :: forall a.a something like this may happen in a large type expressions (and with 'forall' they will become quite large), when one renames variables, and accidentally a type variable might get bounded by the wrong quantifier. 3) is 'forall' going to be used at the type level as well, i.e. would one have to write: data forall a. BinaryTree a = Empty | BT a (BinaryTree a) (BinaryTree a) 3.1 now as far as i understand BinaryTree is of kind * -> * (ie a type constructor), which is different to * would the 'forall' for types range over * only, or both? 4) why is 'forall' needed? could someone plese give an example. thanks yavor -- iavor s. diatchki university of cape town email: [EMAIL PROTECTED] web:http://www.cs.uct.ac.za/~idiatchk
Re: how to replace Num.fromInteger 2
Fri, 19 May 2000 18:59:03 +0400 (MSD), S.D.Mechveliani <[EMAIL PROTECTED]> pisze:
> I wonder how to make the user prelude BPrelude to replace
> 2 + x :: T
>
> with (Additive.fromInteger 2 :: T) + x
> rather than (Num.fromInteger 2 :: T) + x
> ?
I see no better way than making Num a superclass of Additive, and
implement only fromInteger in instances of Num for types that don't
already have one (since you would not use or even import other Num
methods).
--
__("$ P+++ L++>$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e> h! r--%>++ y-
Re: more detailed explanation about forall in Haskell
Fri, 19 May 2000 14:48:24 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> On the other hand someone's remark and about the meaning Haskell gives to
> these two types and I wonder since today if one means by a -> a a type
> indication to be understood as a function having this type signature
> means that the function is only defined for some a 's and by forall a.
> a -> a a type indication to be understood
> as a function that is really defined for ALL type's a .
Not quite. Let's have an example:
rep:: Int -> (a -> a) -> (a -> a)
rep 0 f = id
rep n f = f . rep (n-1) f
What is the type of f inside rep?
It is not "forall a. a -> a". If it was, one could write
rep 0 f = if f True then id else undefined
and it would not have any semantics, because one can pass the function
"\x -> x+1" as the second argument of rep.
It is not "exists a. a -> a". If it was, one could not write the
second equation for rep, because the function "not" should have the
type "exists a. a -> a" too, and it clearly cannot be used instead of
"f" in the second equation. In other words, the fact that exists some
type "a" for which "f" has the type "a -> a" does not guarantee that
this is exacly this "a" that is needed here.
So what is the type of f?
Answer: it is "a -> a", where "a" is bound by the fact that rep is
polymorphic. It is bound by an implicit kind-of-lambda over types
at the definition of rep.
You cannot write such type in a standard Haskell program, i.e. you
cannot change "f" in the body of rep by "(f :: sometype)", for any type
expression "sometype". But this type, depending on instantiation of a
polymorphic function it is used in, clearly exists, has well-defined
semantics, and is extremely useful.
> I am well aware that the predicates (I would prefer to speak about
> functional relations) Free ( ) and Variable( ) are NOT IMPLEMENTED
> yet , so up to now these predicates serve only the purpose of an
> additional documentation ;
They don't have any semantics defined yet. I mean not informal
explanation what they mean, but how they fit into the type system
of Haskell, what are the typing rules.
I'm afraid it cannot be done in any useful way.
> But I think they might be useful.
> E.g. let's trying to say that instead of the function
>
> pr2:: (a, b) -> b
> pr2 (x,y) = y
>
> I wanted a slightly differing function
>
> pr2':: forall a. [forall b `notin Free(a) . (a,b) -> b]
> pr2' (x,y) = y
What do you gain by the restriction of type of pr2', compared to
pr2? How can the body of a function make use of the restriction? If it
cannot, I don't see why to complicate the type system by introducing
useless constructs.
But first, we must know what it means at all.
> With the above I filter out all arguments having a type of the form
> (a, T(a)) ;
f:: forall c. c -> [c]
f y = let g x = pr2' (x, y) in ...
Does the above compile when we replace "..." with something of the
right type (e.g. []), and if so, what is the inferred type of g as
seen inside "..."?
--
__("$ P+++ L++>$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e> h! r--%>++ y-
Re: more detailed explanation about forall in Haskell
Peter Hancock writes: [..] > Please guys, you are making clowns of yourselves. Amen to that! I've just added the above subject line to my kill file, rather than stop reading the Haskell list altogether. --KW 8-) -- : Keith Wansbrough, MSc, BSc(Hons) (Auckland) ---: : PhD Student, Computer Laboratory, University of Cambridge, UK. : : Native of Antipodean Auckland, New Zealand: 174d47'E, 36d55'S. : : http://www.cl.cam.ac.uk/users/kw217/ mailto:[EMAIL PROTECTED] : ::
Re: more detailed explanation about forall in Haskell
This is getting hysterically funny: > *Jan Brosius writes: > * > > > I must put this in the good way; > * > > > > * > > > [forall x . alpha(x)] => alpha(x) is True > * > > > * > > Yes, by instantiation. > * > > * > I disagree. > *You disagree with my agreeing with you? > About what do you agree with me? Please guys, you are making clowns of yourselves. -- Peter Hancock
RE: more detailed explanation about forall in Haskell
Jan Brosius wrote: > look at this example: > > alpha(x) == x is_an Integer => x^2 > -1 > > this is an example of a formula that is true > > *If you want to come up with your own logic, where alpha(x) > is equivalent to > *forall x. alpha(x), then that's fine. > > No, if alpha(x) is a true formula then forall x. alpha(x) is > again a true assertion I think part of the confusion here has to do with the notation alpha(x). The traditional mathematical notation f(x) is ambiguous. It may either refer to an abstraction or an application. In this regard, lambda notation is much superior. What does the alpha(x) here mean? If we assume it is a function like: alpha = \ x . (x is_an Integer => x^2 > -1 ) then it is meaningful to debate whether or not the inner 'x's refer to the same x as the lambda bound x or whether "x is_an integer" creates a new binding. On the other hand, if we assume that alpha(x) is an application of alpha to x then the debate seems to be whether x refers to some value, or whether it is simply a place-holder. Perhaps Jan can clarify what is meant here. --Peter Douglass
Re: more detailed explanation about forall in Haskell
> As Mark Jones has allready said this thread should end or come to a > conclusion. Unfortunately he said more than that . He said that the > discussion was all about the difference a -> a and forall a. a -> a . And > that's not > true . One only has to read the first 2 or 4 emails about this thread of > discussion. I can't resist another comment. I think you are both right here. In Haskell there are no free type variables, it just looks as if there is because of a Haskell convention. If you write f :: a -> a it really means f :: forall a . a -> a So if "a -> a" appears as a type signature it is indeed equal to "forall a . a -> a" because Haskell has implicit forall quantifers for the free type variables of a signature. On the other hand, if we talk about a subexpression having type "a -> a" (which there is no syntax for in Haskell) this does not imply that it has type "forall a . a -> a", but rather that it has a type where the variable "a" has been bound in some outer scope. I think the source of all this debate is the convetion that type variables are implicitely quantified. I agree with Jon here, it was a mistake. -- Lennart
replacing numeric literals
I wrote in previous letter on replacing (Num.fromInteger 2 :: T) + x with(Additive.fromInteger 2 :: T) + x It occurs to me now that, probably, the popular preprocessors are for such purposes. But I never tried ... -- Sergey Mechveliani [EMAIL PROTECTED]
Re: more detailed explanation about forall in Haskell
I also think it is hopeless , but I still want to try again *- Original Message - *From: Frank Atanassow <[EMAIL PROTECTED]> *To: Jan Brosius <[EMAIL PROTECTED]> *Cc: Frank Atanassow <[EMAIL PROTECTED]>; <[EMAIL PROTECTED]> *Sent: Friday, May 19, 2000 12:59 PM *Subject: Re: more detailed explanation about forall in Haskell *Jan Brosius writes: * > > > I must put this in the good way; * > > > * > > > [forall x . alpha(x)] => alpha(x) is True * > > * > > Yes, by instantiation. * > * > I disagree. *You disagree with my agreeing with you? About what do you agree with me? * > > > If alpha(x) is TRUE then the following is true : alpha(x) => [forall x. * > > > alpha(x)] * > > * > > No, alpha(x) only asserts that some element named x satisfies alpha. It * > does * > > not follow that therefore every other element also satisfies alpha. *> * > No the variable x means that it can be substituted by any term. That is the * > real meaning of a variable * > (at least in classical logic). *Only when the variable is bound by a forall. It is exactly the same situation *as with lambda-calculus and lambda. The term "x" denotes a fixed element of *its type. When I bind it, as in "\x -> x", I'm saying that that x may range *over any element in the type. Once I've said that, yes, I can substitute any *element for x in the body. * (\x -> P(x)) t = P(x) [t/x] * > Consider e.g. Carl Witty's formula : prime(x) == x is a prime number. * > Then prime(2) == (2|x) prime(x) is true , and prime (4) is false * > * > Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies * > not) * > *> then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)] *> * > On the contrary beta(x) == ¬ alpha(x) is true for any x *Yes, because x is bound in the body of beta. I have seen what you mean by bound. Clearly you are talking about something else than quantified logic * beta := \x -> not(alpha(x)) You are talking about lambda calculus where I am talking about quantified logic *BTW, I don't understand your "(2|x)" notation. Is this a substitution? Yes * > > > So if alpha(x) is TRUE then [forall x. alpha(x) ]<=> alpha(x) * > > * > > This does not follow. It is truth-equivalent to: * > * > Sorry, I disagree *Well, you certainly have the right to disagree. But you are disagreeing with *every logician since Gentzen. I disagree with you Frank , the rest is your imagination. * > > [forall x. alpha(x)] <=> True * > * > ( In the above you should at the very least not forget to mention that * > [forall x. alpha(x)] must be true ) *Isn't that what I wrote? Of course not , what you wrote down is FALSE stated like that. Don't you see that? * > > I repeat: you do not understand the difference between bound and free * > variables. * > * > I disagree a free variable is not a constant. *> > A free variable behaves like a constant. * > * > No a constant is always the same constant, it is never substituted by * > something else, it is "immutable". * > * > A variable is a placeholder for a Term ( a constant is a special term) *I see where you are heading. In the reduction laws, you substitute for free *variables. This is true, but you can only substitute for a free variable if it *was bound in an outer scope, and you are stripping off the binding, as in the *beta-equality for lambda-calculus, which I will repeat: I am not talking about reduction laws * (\x -> P(x)) t = P(x) [t/x] *You cannot simply substitute any value you please for an arbitrary free *variable and expect the new term to be equal to the old one. For example in *Haskell, fst :: (a,b) -> a is a free variable in every term (where it's not *shadowed). Now if I have the term * fst p *and I substitute snd for fst: * (fst p) [snd/fst] = snd p *but * fst p /= snd p *which demonstrates that substitution on free variables is not sound in *general. No you still don't understand me * This is the reason for abstraction: it asserts that a free variable *in the scope of the abstraction can range over the whole domain, so any *substitution will preserve equality. It is exactly the same with forall. * > >It is not "implicitly" * > > quantified in any way, because it denotes a specific element. The only * > > difference between a constant and a free variable is syntactic: a free *> > variable can be bound in an outer scope, * > * > No the real role of a variable say x in a formula alpha(x) or a term T(x) * > is a PLACEHOLDER ready to be substituted by a Term (e.g. constant or a * > parameterized term) * > * > And that's the reason why I should find it weird if In Haskell 98+ one * > would distinguish between * > * > a -> a and [forall a. a -> a] * > * > >while a constant cannot. * > > * > > > > The sentence "alpha(x)" asserts that there is a _distinguished_ * > element * > > > > named * > > > * > > > NO , saying that there is a distinguished element T that satisfies * > alpha * > > > implies * > > > *
how to replace Num.fromInteger 2
I wonder how to make the user prelude BPrelude to replace 2 + x :: T with (Additive.fromInteger 2 :: T) + x rather than (Num.fromInteger 2 :: T) + x ? For BPrelude hides Num and moves +, fromInteger ... to Additive. So, the compiler reports "(Num T) is required". Maybe, the compiler can be told what to substitute for the numeric literals? The language would hardly care for this. I do not know whether RULES can help, but the thing still has to work under Hugs too. Thanks in advance for the idea. -- Sergey Mechveliani [EMAIL PROTECTED]
Re: Block simulation / audio processing
> Has anyone built any block simulators (for modeling continuous
> electronic systems, like OP Amps, RC networks, etc) in Haskell?
There have been several replies to this already, but permit me to add my
2 cents worth:
FRP ("Functional Reactive Programming") is an abstraction of Fran
("Functional Reactive Animation") that is ideally suited to describing
such things, since it is based on continuous (time-varying) values, as
opposed to discrete values. You can find out a lot about Fran from
Conal Elliott's home page (http://www.research.microsoft.com/~conal) and
from my book (http://haskell.org/soe), and about FRP at
http://haskell.org/frob. My student Zhongong Wan and I also have a new
PLDI paper on the formal underpinnings of FRP if anyone is interested
(it's not on the web yet).
As for Haskore:
> I'm also interested in this. I am thinking of extending
> Paul Hudak's Haskore system to generate and handle true audio data
> (instead of, or in addition to) MIDI data.
>
> I don't think I'll have enough time to do the programming myself,
> but since I'll be using Hudak's book in next term's course,
> I hope I can attract some students, and set them in the right
> direction.
>
> In fact one student who read the course announcement
> (and the book's web page) already asked me
> about functional audio signal processing.
The latest release of Haskore (http://haskell.org/haskore) includes an
interface to Csound. That is, one can wire up oscillators, modulators,
special effects, etc. in a nice declarative style in Haskell, which then
gets compiled into a Csound instrument file, which in turn gets compiled
by Csound into actual sound files (.wav, .snd, etc.). The nice thing
about this is that it's fairly efficient because of the back-end
processing. To do this in FRP would be much less efficient.
Hope this helps,
-Paul
RE: more detailed explanation about forall in Haskell
Frank Atanassow wrote: > However, I think maybe it has demonstrated that the implicit > forall'ing in > Haskell can be confusing in practice. In particular, it makes > it hard to talk > unambiguously about types of non-top-level definitions/terms. I'm sure this pot has been stirred up enough already, but as a newbie to Haskell I also found the "forall" rules counter-intuitive with regard to exitential types. (i.e. the use of forall a. when exists a. might have been clearer.) I hope that at some point this area of Haskell will be revised. --Peter Douglass
Re: more detailed explanation about forall in Haskell
|From: Lennart Augustsson <[EMAIL PROTECTED]> |To: Jan Brosius <[EMAIL PROTECTED]> |Cc: Frank Atanassow <[EMAIL PROTECTED]>; <[EMAIL PROTECTED]> |Sent: Friday, May 19, 2000 12:07 PM |Subject: Re: more detailed explanation about forall in Haskell > Jan Brosius wrote: > > > > "x" in the domain of your model, and that that element, at least, > > satisfies > > > > x is a variable ; no domain ; no model > > You must have some assumed convention that makes x a variable. That's true . To be complete in Bourbaki's formal logic they don't speak in the beginning about a variable but they define a substitution mechanism for ONLY small latin letters ,denoted ( T | u) S which means replace in S , being just consecutive string of symbols, every occurence of the letter u by T , which itself is also a consecutive string of symbols , I think this corresponds to (T | u) S == (lambda u . S) T (as far as I know lambda- calculus) Of course they begin with a set of allowable symbols. Later when they talk about a mathematical theory they introduce the "metha-mathematical " notion of variable in the following sense a letter t is a variable of the theory if this letter does not occur explicitly in one of the axioms of the theory. Another way to introduce a variable would be to use a special letter say x and to say, that a variable is an x subscripted by an integer number , this would mean that only x0 , x1 , x2 , ... ,x10 , etc. .. are variables. But this is not the place to explain in full detail Bourbaki's approach of formal logic . I thought there is a common consensus in logic about a variable. Allow me to come back to to some meaning of variable expressed by someone else in a previous email. A person said something like this " alpha(x) means that alpha(x) is true for some x " (where alpha(x) denotes a formula containing a variable x .) Now if one looks carefully this above sentence means formally [exists x. alpha(x) is true] which is a FALSE assertion. To be honest he didn't wrote the above english phrase not like this , but he represented it by the implication alpha(x) => [exists x . alpha(x)] which is a totally other thing . This implication should more be read as " if alpha(x) is true for some x then there exists an x such that alpha(x) is true" Now as everybody can see the above phrase looks a bit strange . It would have been better to replace it by (T | x) alpha(x) => [exists x . alpha(x)] where T is a TERM not containing the letter x which can be read " if alpha(x) is true for some x = T then there exists an x such that alpha(x) is true " which is perhaps an english phrase that makes more sense (I don't know) . Bourbaki uses this implication ( (T | x) alpha(x) => [exists x . alpha(x)] where T is a TERM not containing the letter x ) as an axiom scheme for his theory with quantifiers . Bourbaki makes a distinction about axioms and speaks about explicit axioms and axiom schemes. But the above remarks would have lead the discussion off the road and also not everybody knows about Bourbaki. When I referred to variables and to the forall quantifier I implicitly thought that there was a common consensus about the use of variables and the forall quantifier. Now it doesn't bite me if someone regards variables as ranging over a domain . But I had to reply since one was insinuating that I don't understand the difference between free and bound variables , that is saying as much as : you don't understand logic. As Mark Jones has allready said this thread should end or come to a conclusion. Unfortunately he said more than that . He said that the discussion was all about the difference a -> a and forall a. a -> a . And that's not true . One only has to read the first 2 or 4 emails about this thread of discussion. On the other hand someone's remark and about the meaning Haskell gives to these two types and I wonder since today if one means by a -> a a type indication to be understood as a function having this type signature means that the function is only defined for some a 's and by forall a. a -> a a type indication to be understood as a function that is really defined for ALL type's a . The above is just a question . If my interpretation is right then one can change a -> a by [exists a. a -> a] But again my first email didn't talk about that , as every reader willing to look in the archives would acknowledge. Friendly Jan Brosius PS : by saying weird I didn't mean illigitimate I meant more something like "it surprises me" where I am talking as a mathematician trying to use Haskell , not knowing the type system that is used nor the theory behind it , only being surprised that in some cases forall cannot be understood anymore as forall in formal logic. E.g. it is a true fact that Bourbaki doesn't use forall before a type , and I thought it is common consensus in formal logic used in math that one doesn't use a forall for a term. So I
Re: more detailed explanation about forall in Haskell
> Please could somebody post a short, plain text summary of the discussion > in this thread? The recent exchanges have been long and involved, which > has made it impossible for me (and other busy onlookers too, I suspect) > to keep up. Without such a summary, I think that this thread may be > reaching the end of it's useful life, at least for the main Haskell list. I won't attempt a full summary, but in spite of some unfortunate personal excesses (recent messages let me hope that they won't be repeated..) and some unnecessary copying and repeating of messages, the basic issues seem to have become a bit clearer now. So I'll try to summarize those. The thread started in connection with the typing of state transformers (especially runST and friends) but by now, I assume that the difficulties are solely down to (different schools of) logic. The baseline is that there are several interpretations of common syntax in use which, in isolation, may or may not be consistent, but certainly lead to confusion and inconsistencies if mixed. Our main problem is that we are not always aware that each poster might associate different assumptions when using the same syntax. Jan Brosius seemed to claim that, for a formula context alpha (1)forall x. alpha(x) <=> alpha(x) which seemed wrong to others, who suspected that misunderstandings in scoping were the issue. Some progress was made when it was suggested that different interpretations of open formulae (formulae with free variables) and equivalence might be involved. The claim was then modified to: (2)"forall x. alpha(x)" is a TRUE formula iff "alpha(x)" is a TRUE formula >From the context in which the concept of a "TRUE formula" was used, I assume the definition: (3) "a" is a TRUE formula iff [definition] "a" is true in all interpretations (substitutions for free variables). Note that definition (3) validates (2), but doesn't require a contextual equivalence of the quoted formulae, so it does not follow that (4)forall contexts C and alpha. ( "C[forall x. alpha(x)]" is a TRUE formula iff "C[alpha(x)]" is a TRUE formula) Most of the disputed examples were stated in such a form that Jan could assume an empty context whereas others assumed an implied quantification over all contexts. Many misunderstandings should disappear if contexts are made explicit. E.g., for Jan, (1) was just a bad way to write down (2), whereas others interpreted (1) as (5)forall contexts C and alpha. (C[forall x. alpha(x)] <=> C[alpha(x)]) Naturally, Jan concluded that (1) is valid, if badly written, whereas others concluded that (1) is invalid. Similarly for the more complex examples. A second source of confusion was whether free variables should be interpreted or not. One school of reasoning assumes that variables are placeholders for elements of a certain domain, another (apparently favoured by Jan) assumes that variables are placeholders, period. With uninterpreted free variables, "alpha(x)" can only be true if "alpha" is completely independent of its parameter (we can execute the rules of the logic purely syntactically and never need to make any assumption about the variable "x" when evaluating "alpha(x)"). For the "uninterpreted" school, (1) is valid, because we can derive additional information about "alpha(x)", namely that it has to be completely parametric in "x". This additional information is not available in the "interpreted" school: if we assume that variables and formulae have to be interpreted in some domain, we either have to reject open formulae alltogether or assume an implicit quantification over free variables, as in (3). But then, the question becomes where to put the implicit quantifiers in (1): (6a) "forall x. alpha(x) <=> FORALL x. alpha(x)" (6b) "FORALL x. (forall x. alpha(x)) <=> alpha(x)" (6a) interprets "<=>" as part of the meta-logic [so there are two formulae in (1), to be quantified individually], whereas (6b) interprets "<=>" as part of the object-logic [so there is only a single formula in (1)]. (6a) is valid, (6b) is not.. Again, this leads to ambiguities and to completely different conclusions about the more complex examples and counterexamples. The nasty part of this was that the opponents used seemingly familiar notation (and so assumed that no definition was required), yet associated completely different interpretations with a common notation. In fact, while I am reasonably confident that the above identifies some of the relevant issues, I am not at all sure whether this solves all misunderstandings, or whether I have expressed myself in such a way that all parties involved come to the same interpretation of this message. Claus PS. These issues must come up again and again when teaching or learning logic. If anyone knows a good study/survey of "common misunderstandings in introductory logic courses", I would be grateful for a refere
FSTTCS 2000: revised Call for Papers
--text follows this line-- *** * * *FST TCS 2000 * * * * Foundations of Software Technology and Theoretical Computer Science * *December 13--15, 2000* * New Delhi, India * * * *** * Call for Papers* *** New: Electronic Submission Guidelines Revised list of Invited Speakers ** IARCS, the Indian Association for Research in Computing Science, announces the 20th Annual FST TCS Conference in New Delhi. Tentatively planned satellite events include include two workshops: on Computational Geometry and on Advances in Programming Languages. Authors are invited to submit papers presenting original and unpublished research on **any** theoretical aspects of Computer Science. Papers in applied areas with a strong foundational emphasis are also welcome. The proceedings of the last six years' conferences (Springer-Verlag Lecture Notes in Computer Science volumes 880, 1026, 1180, 1346, 1530, 1738) give an idea of the kind of papers typically presented at FST TCS. Typical areas include (but are not restricted to): Automata, Languages and Computability Randomized and Approximation Algorithms Computational Geometry Computational Biology Combinatorial Optimization Graph and Network Algorithms Complexity Theory Parallel and Distributed Computing New Models of Computation Concurrent, Real-time and Hybrid Systems Logics of Programs and Modal Logics Database Theory and Information Retrieval Automated Reasoning, Rewrite Systems, and Applications Logic, Proof Theory, Model Theory and Applications Semantics of Programming Languages Static Analysis and Type Systems Theory of Functional and Constraint-based Programming Software Specification and Verification Cryptography and Security Protocols For an accepted paper to be included in the proceedings, one of the authors must commit to presenting the paper at the conference. Important Dates --- Deadline for Submission 31 May, 2000 Notification to Authors 15 August, 2000 Final Version of Accepted Papers due15 September, 2000 Deadline for Early Registration 15 November, 2000 Submission Guidelines - - Authors may submit drafts of full papers or extended abstracts. Submissions are limited to 12 A4-size pages, with 1.5 inch top margin and other margins 1 inch wide with 11 point or larger font. Authors who feel that more details are necessary may include a clearly marked appendix which will be read at the discretion of the Programme Committee. Each paper should contain a short abstract. If available, e-mail addresses and fax numbers of the authors should be included. Electronic Submissions - Electronic submission is very strongly encouraged. You may submit your paper using Rich Gerber's system START by visiting the URL for the conference and following the appropriate links. The URL for submissions is http://www.cse.iitd.ernet.in/~fsttcs20/START/www/submit.html In case you ar eunable to submit using START, self-contained uuencoded gzipped Postscript versions of the paper may be sent by e-mail to [EMAIL PROTECTED] In addition, the following information in ASCII format should be sent to this address in a **separate** e-mail: Title; authors; communicating author's name, address, and e-mail address and fax number if available; abstract of paper. Hard-Copy Submissions - - If electronic submission is not possible, authors may submit five (5) hard-copies of the paper by post to the following address: FST TCS 2000 Department of Computer Science and Engineering I.I.T., Delhi Hauz Khas New Delhi 110 016 INDIA Invited Speakers Invited Speakers who have confirmed participation include: Peter Buneman (U Penn) Bernard Chazelle (Princeton) E. Allen Emerson (U Texas, Austin) Martin Groetschel (ZIB) Jose Meseguer (SRI) Philip Wadler (Bell Labs) Programme Committee ---
Re: more detailed explanation about forall in Haskell
On 19 May 2000, Ketil Malde wrote: > Frank Atanassow <[EMAIL PROTECTED]> writes: > > > I agree, and I think it's hopeless. This is my last message to the Haskell > > list on the subject. There is nothing Haskell-specific any longer about this > > discussion. > > Uh, I feel I'm a bit of a hobbyist on this list, but what exactly is > the relevance of all this? Flipping through these messages, I feel I > have aquired some grasp of forall, but in what contexts is forall used > in Haskell - can anybody point me to an URL that explains or > exemplifies? > How about: http://haskell.org/onlinereport/decls.html http://www.haskell.org/ghc/docs/latest/users_guide/universal-quantification.html http://www.cse.ogi.edu/PacSoft/projects/Hugs/pages/hugsman/exts.html http://www.cs.chalmers.se/~augustss/hbc/decls.html /Lars L
Re: more detailed explanation about forall in Haskell
There is a good introduction by Cardelli and Wegner:
Luca Cardelli and Peter Wegner. On understanding types, data abstraction,
and polymorphism. Computing Surveys, 17(4):471-522, 1985.
available from Cardelli's page at
http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.A4.ps
http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.{US,A4}.{ps.pdf}
--
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
Frank Atanassow <[EMAIL PROTECTED]> writes: > I agree, and I think it's hopeless. This is my last message to the Haskell > list on the subject. There is nothing Haskell-specific any longer about this > discussion. Uh, I feel I'm a bit of a hobbyist on this list, but what exactly is the relevance of all this? Flipping through these messages, I feel I have aquired some grasp of forall, but in what contexts is forall used in Haskell - can anybody point me to an URL that explains or exemplifies? -kzm -- If I haven't seen further, it is by standing in the footprints of giants
RE: more detailed explanation about forall in Haskell
Mark P Jones writes: > Please could somebody post a short, plain text summary of the discussion > in this thread? The recent exchanges have been long and involved, which > has made it impossible for me (and other busy onlookers too, I suspect) > to keep up. Without such a summary, I think that this thread may be > reaching the end of it's useful life, at least for the main Haskell list. I only jumped in because I thought I could nip it in the bud by clearing up some confusion surrounding treatment of bound and free variables (OK--- also I was irate about one other remark). Sorry, I can't summarize the rest, although I think it is all rooted in this misinterpretation of variables. > I make these suggestions because I sense that there is a lot of confusion, > misunderstanding, and talking at cross purposes, and because I'm not at > all sure that the current discussions are on course to reach a conclusion. I agree, and I think it's hopeless. This is my last message to the Haskell list on the subject. There is nothing Haskell-specific any longer about this discussion. However, I think maybe it has demonstrated that the implicit forall'ing in Haskell can be confusing in practice. In particular, it makes it hard to talk unambiguously about types of non-top-level definitions/terms. -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
Jan Brosius writes: > > > I must put this in the good way; > > > > > > [forall x . alpha(x)] => alpha(x) is True > > > > Yes, by instantiation. > > I disagree. You disagree with my agreeing with you? > > > If alpha(x) is TRUE then the following is true : alpha(x) => [forall x. > > > alpha(x)] > > > > No, alpha(x) only asserts that some element named x satisfies alpha. It > does > > not follow that therefore every other element also satisfies alpha. > > No the variable x means that it can be substituted by any term. That is the > real meaning of a variable > (at least in classical logic). Only when the variable is bound by a forall. It is exactly the same situation as with lambda-calculus and lambda. The term "x" denotes a fixed element of its type. When I bind it, as in "\x -> x", I'm saying that that x may range over any element in the type. Once I've said that, yes, I can substitute any element for x in the body. (\x -> P(x)) t = P(x) [t/x] > Consider e.g. Carl Witty's formula : prime(x) == x is a prime number. > Then prime(2) == (2|x) prime(x) is true , and prime (4) is false > > Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies > not) > > then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)] > > On the contrary beta(x) == ¬ alpha(x) is true for any x Yes, because x is bound in the body of beta. beta := \x -> not(alpha(x)) BTW, I don't understand your "(2|x)" notation. Is this a substitution? > > > So if alpha(x) is TRUE then [forall x. alpha(x) ]<=> alpha(x) > > > > This does not follow. It is truth-equivalent to: > > Sorry, I disagree Well, you certainly have the right to disagree. But you are disagreeing with every logician since Gentzen. > > [forall x. alpha(x)] <=> True > > ( In the above you should at the very least not forget to mention that > [forall x. alpha(x)] must be true ) Isn't that what I wrote? > In principle True is a sloppy expression for saying that [forall x . > alpha(x)] is a theorem of some mathematical theory. I have used True because > discussing mathematical theories would have lead the discussion > out of the scope of the discussion. > > For instance let "T=" denote a mathematical theory with equality > > then one has "T=" -| x = x > > that is the formula x = x is a theorem in "T=" . More sloppy the formula > x=xis TRUE in "T=" This has no bearing on the discussion. > > which is equivalent to: > > > > forall x. alpha(x) > > > > which is only true when every element satisifies alpha; so it is not a > > tautology. > > > > I repeat: you do not understand the difference between bound and free > variables. > > I disagree a free variable is not a constant. I didn't say it _was_ a constant. I said it behaved like a constant, but that they are syntactically distinct because you cannot bind a constant. > A bound variable is a variable tied to a quantifier. In principle a bound > variable is not visibly. > This is best illustrated by Bourbaki's approach where they first define : > > exists x . alpha(x) == (`t x (alpha)| x) alpha > > where if e.g. alpha(x) == x = x then > > `t x (alpha) == `t ( `sq = `sq ) where `sq denotes a small square and > where here both `sq are tied to `t by a line > In this way I can really say that in [existx x. x = x] the variable x has > disappeared. > > Finally Bourbaki defines forall x . alpha(x) == ¬ [exists x . ¬ alpha(x)] Sorry, I don't understand your notation, or what relevance this has. > I repeat : there are no domains in propositional calculus , but I am aware > that in some text books about > propositional calculus one speaks about it , I regard this as cheating : > introducing a concept that one is going to define later. I remember my > prof, in logic in 1 cand. math - physics where his first lesson began by > writing > on the blackboard : p V ¬ p and he only said " p or not p " " tertium > non datur" " a third possibility is not given " > His whole course was as formally as possible, and variables were not > supposed to range about a domain. I don't understand what relevance this has. > > A free variable behaves like a constant. > > No a constant is always the same constant, it is never substituted by > something else, it is "immutable". > > A variable is a placeholder for a Term ( a constant is a special term) I see where you are heading. In the reduction laws, you substitute for free variables. This is true, but you can only substitute for a free variable if it was bound in an outer scope, and you are stripping off the binding, as in the beta-equality for lambda-calculus, which I will repeat: (\x -> P(x)) t = P(x) [t/x] You cannot simply substitute any value you please for an arbitrary free variable and expect the new term to be equal to the old one. For example in Haskell, fst :: (a,b) -> a is a free variable in every term (w
Re: more detailed explanation about forall in Haskell
Jan Brosius wrote: > > "x" in the domain of your model, and that that element, at least, > satisfies > > x is a variable ; no domain ; no model You must have some assumed convention that makes x a variable. For the rest of us it might as well be a constant, because there is no way to tell if it is a variable or not. -- -- Lennart
Re: Block simulation / audio processing
Mike Jones wrote: >.. . My be problem is how to > dynamically control the step size of algorithms to support algorithms that > have non-uniform step size. Perhaps some kind of clock divider scheme. In general this is one of the gray areas between continuous (discretized anyway) and discrete (clocked) simulations. Synchronous, clocked approach is less than well adapted to this sort of problems, because the link between the global clock time and the local discrete time for an adaptive DE algorithm ceases to exist. Yes, why not division? Or just, if you are interested in the final solutions as trajectories and *not* as sequences of events, you forget about clocks. (This is my very naive and minima- listic viewpoint...) The *strictly technical* problem on how to control the step size depends on the algorithm. I wonder whether there are some generic strategies here. Jerzy Karczmarczuk Caen, France
Re: Block simulation / audio processing
Koen Claessen wrote:
> The reason we removed the monads was that circuits with
> feedback (loops) in them became very tedious to define. One
> had to use monadic fixpoint operators (or "softer" variants
> on them), which were really unnatural to use. Also, the
> monadic style enforces an ordering on the components that
> you are using, while in a circuit, there is no such ordering
> (everything works in parallel).
I always thought that monads (or just more concretely: CPS) *help*
to sequentialize the processing of streams, but that one is
never obliged to put them where unneeded.
Loops ("short" loops which in Matlab are called "algebraic")
either must be sequentialized anyway, or - as in Matlab - they
generate some equations which must be solved globally; one gets
into something like constraint programming.
I wonder what is the Lava approach to those loops then. OK, I will
read the cited paper. For the moment Koen mentioned that the system
"detect" loops. And the real fun *begins* here...
Jerzy Karczmarczuk
Caen, France
