- Haskell-Cafe - Haskell.org

Re: Question about the use of an inner forall
by Jon Cast 21 Aug '02

21 Aug '02

"Scott J." <jscott(a)planetinternet.be> wrote: > Hi, > I am going to stop this discussion . What counts for me at this > moment is that I know how it works. Alright. > I thank everybody who replied to my email. You're welcome. > As for the discussion about Curry Howard isomorphism and more about > type theory, I shall gladly discuss these things further but than in > private email. Do you mean ``but in private email''? Why? I think that, because of the strong mathematical basis underlying Haskell, these things are on-topic. So, why not let the list profit from the discussion? > Hey, I hope really that I know how it works but this seems to be > confirmed in these emails. > I left Ocamel for Haskell for it's more functional approach. > I think documentation about the features extending Haskell 98 is > very needed for those who want only to program with the > language Haskell. True; unfortunately, too many extensions are documented only in technical papers... > Thx for all replies > Scott Jon Cast

5 6

Leical and syntactic analyzer
by Jonata Goulart 21 Aug '02

21 Aug '02

Does somebody know where can I find an example of a lexical and syntactic analyzer for arithmetic and conditional statements in Haskell? Thanks _________________________________________________________________ Chat with friends online, try MSN Messenger: http://messenger.msn.com

1 0

Re: Fw: Question about the use of an inner forall
by oleg＠pobox.com 20 Aug '02

20 Aug '02

> Leon Smith wrote: > >On Friday 16 August 2002 23:57, Scott J. wrote: > >runST :: forall a ( forall s ST s a) -> a ? > > > >In logic forall x forall y statement(x.y) is equivalent to: > > forall y forall x statement(x,y). > Now, using a different argument, since "s" does not appear free on > the R.H.S of the implication, "forall s" can be moved outside the > implication to quantify over the entire type. I'm afraid I disagree -- in general, we can't move quantifiers in and out with impunity. In our example: all a. ( (all s. ST s a) => a ) === all a. ( !(all s. ST s a) | a ) === all a. ( (exists s. !(ST s a)) | a ) === {using identity (exists x. p) | q === exists x. (p|q) where x is not free in q} === all a. (exists s. (!(ST s a) | a)) === all a. exists s. (ST s a => a) So, the type of runST is runST::exists s. (ST s a -> a) Alas, we can't use 'exists' quantifier in type expressions; therefore, we have to use the round-about trick with forall, on the _left-hand_ side of the implication. > Jon Cast wrote: > Polymorphic types form a sub-typing system, with the basic > sub-typing judgment: > (forall a. S) < [T/a]S I'd like to note a parallel with lambda-Prolog: If S is the set of type declarations and P is the set of program clauses, to prove (forall x::T. G) from <S,P>, we introduce a new unique _constant_ c of type T and attempt to prove [c/x]G from <S U {c},P> OTH, to prove (exists x::T . G) from <S,P>, we prove [_X/x]G from <S,P> where _X is just a (unbound) Prolog variable. We let the standard unification mechanism to bind _X to something that makes G true. On the subject of escaping of quantified variables, the lambda-Prolog Tutorial by Amy Felten gives an interesting example: ?- append (1::2::nil) z X. the answer is X == (1::2::z). ?- pi y\( append (1::2::nil) y X). the answer is NO. Indeed, as outlined before, we first choose a unique constant k and attempt to prove ?- append (1::2::nil) k X. The proof seemingly succeeds, with X bound to (1::2::k). However, this binding causes 'k' to 'escape'. Therefore, this binding is rejected, and the proof falls apart. Which indeed makes sense: the value of X that makes pi y\( append (1::2::nil) y X) true should not depend on any particular value of y. Only in this case the expression would be true for all y. ?- pi y\( append (1::2::nil) y (H y)). actually succeeds, with H bound to w\(1::2::w).

1 0

Re: Question about sets
by Jon Cast 20 Aug '02

20 Aug '02

"Scott J." <jscott(a)planetinternet.be> wrote: > As far a I know sets can implemented by implementing a list of > anything(a list of all types) The sets Haskell does have are AFAIK > sets of elements of the same type: these are not general sets. Ah. That's a static typing issue. However, I don't think it's really an issue. In axiomatic set theory, every set must be a subset of some other set, except for powersets and unions. Unions are implementable using Either, and powersets are implementable using Set (i.e., powerset :: Set a -> Set (Set a)). > Scott Jon Cast

1 0

questions
by Jonata Goulart 20 Aug '02

20 Aug '02

I'm trying to do a simple lex analyser in haskell I defined the function lexi that is intended to break a string into tokens returning them as a list but I received the following error: ERROR "TesteEval.hs":20 - Syntax error in input (unexpected symbol "restante") isLetter:: Char -> Bool isLetter c = or [isLower (c), isUpper (c)] isLetterorDigit:: Char -> Bool isLetterorDigit c = or [isLetter (c), isDigit (c)] main = lexi lexi " "= [] lexi (a:x) | isLetter a = token: lexi restante where S = takeWhile isLetterorDigit x line 20 ------> restante = dropWhile isLetterorDigit x token = 'Id' ++ S _________________________________________________________________ Chat with friends online, try MSN Messenger: http://messenger.msn.com

2 1

Questions about sets
by Scott J. 20 Aug '02

20 Aug '02

As far a I know sets can implemented by implementing a list of anything(a list of all types) The sets Haskell does have are AFAIK sets of elements of the same type: these are not general sets. Scott

1 0

Question about the use of an inner forall
by Scott J. 19 Aug '02

19 Aug '02

Hi, I am going to stop this discussion . What counts for me at this moment is that I know how it works. I thank everybody who replied to my email. As for the discussion about Curry Howard isomorphism and more about type theory, I shall gladly discuss these things further but than in private email. Hey, I hope really that I know how it works but this seems to be confirmed in these emails. I left Ocamel for Haskell for it's more functional approach. I think documentation about the features extending Haskell 98 is very needed for those who want only to program with the language Haskell. Thx for all replies Scott

1 0

Re: Question aboutthe use of an inner forall
by Jon Cast 19 Aug '02

19 Aug '02

"Scott J." <jscott(a)planetinternet.be> wrote: > Well I don't feel alone anymore. > Here follows how I think runST :: (forall s. ST s a) -> a works: > if a is represented by e.g. MutVar s a . Then the compiler complains > because it did find an s in the "data" represented by a. This s must > first be eliminated by some other combinators(?). Right. The `s' is appearing outside the area it is defined in. > I agree that something must be written for the argument of runST to > warn programmers about the possible "representations" of a. But I > still have problems that one has chosen forall. `forall' and `Pi' are the basic names for this sort of thing in type theory. See the discussion of the Howard-Curry isomorphism for `forall'. You probably don't want to know about `Pi'. > Scott Jon Cast

1 0

Re: Question aboutthe use of an inner forall
by Jon Cast 19 Aug '02

19 Aug '02

Jay Cox <sqrtofone(a)yahoo.com> wrote: > From: "Ashley Yakeley" <ashley(a)semantic.org> > > At 2002-08-16 20:57, Scott J. wrote: > > >However what for heaven's sake should I think of > > >runST :: forall a ( forall s ST s a) -> a ? > > runST :: forall a. ((forall s. ST s a) -> a) > > "For all a, if (for all s, (ST s a)) then a." > > You may apply runST to anything with a type of the form (forall > > s. ST s a), for any 'a'. > I'm very fuzzy to the details of type theory in general so please > forgive any errors. > I noted the same question as Scott's when I first learned about > ST threads. > When you have a rank-2 polymorphic function, like > runST::forall a . ( forall s . ST s a) -> a > the type means the function takes an argument ***at least as > polymorphic*** as (forall s . ST s (some type a independent of s)). I'm not sure I understand polymorphic types, but here's my best guess: Polymorphic types form a sub-typing system, with the basic sub-typing judgment: (forall a. S) < [T/a]S where T and S are types, and a may occur free in S, and (<) is the sub-typing relation. From this comes the typing judgment S < T x :: S ----------------- x :: T For the purposes of runST, we only need to worry about one other judgment, the standard judgment for sub-typing function arguments: S < T ------------------- (T -> R) < (S -> R) Justification: basically, the sub-typing statement (S < T) says that every element of S is an element of T. The typing statement (f :: S -> R) says that f can take any value of type S and deliver a value of type R (divergence is a value in Haskell!). Now, if every element of S is an element of T, and f can take every element of T, it follows that f can take every element of S. (x :: S) -> (x :: T) (x :: T) -> (f x :: R) ---------------------------------------------------- (x :: S) -> (f x :: R) is an equivalent way of stating the above judgment. So, runST's types are the super-types of (forall a. (forall s. ST s a) -> a), which means all functions types for which the argument is a super-type of (forall s. ST s a). Does that clarify things any? <snip> Jon Cast

1 0

Re: Question aboutthe use of an inner forall
by Jon Cast 19 Aug '02

19 Aug '02

"Scott J." <jscott(a)planetinternet.be> wrote: > Ok, a and s are type variables. It may be common usage for computer > people Bingo. You're trying to impose a non-CS understanding on a CS statement. If you're familiar with the analogy, it's like a French speaker trying to insist that ``demand'' in English cannot mean an insistence, since it doesn't mean that in English. > but for someone with a math background it is difficult Get used to difficulty. Seriously. > to call forall a a type . In logic one expects a statement in the > scope of forall a like this forall a is not a type (nor a statement) :) It's a phrase in any number of languages, including formal logic and type theory (and it has different, although cognate, meanings in those languages). > (forall a) statement. The statement may or may not depend on a. True. But if you have (forall a. type), that doesn't fit your form. And, just like (forall a. statement) is a statement, (forall a. type) is a type. Easy, no? > So let's come backe to runST. > runST ::( forall s) (ST s a )-> a May I ask a favor? If you're going to discuss type theory, learn our notation: > runST :: (forall s. ST s a) -> a Just a minor nit. > So I insist what is the statement ST s a ? It's not a statement, and forall s. is not a logic quantifier. ST s a is a type, and forall s. is a type quantifier. > Scott Jon Cast

1 0