- Haskell-Cafe - Haskell.org

Re: monads, modules, sandboxes
by Richard Uhtenwoldt 21 Aug '02

21 Aug '02

this will be my last message on this topic as I need to stop reading this list for a few months. Alastair Reid writes: >A potential difference (which Richard Uhtenwoldt hints at) is that it >can be hard to control the flow of OS capabilities as the capability >is passed from one process to another to another. This gets >especially tricky when you want policies like 'X can either read files >or use the network but not both' (so X cannot leak secrets learnt from >the filesystem). I think this is why capability OSs have fallen out >of favour in the OS community. I suspect that typesystems are better >able to express and enforce these policies. seems to me capabilities can do that: you just pass to X a capability (pointer) to an object that will return either a read-only capability to the filesystem or a capability to the network inferface but not both. either that or use the revocable-capability pattern twice in such a way that before the first network access happens, the filesystem capability is revoked and before the first filesystem read happens the network access capability is revoked. to flesh out that first alternative a little, the object passed to X could probably be coded up by modifying the following E language function (found at http://www.erights.org/elang/concurrency/race.html) for making "use-once" capabilities. and yes I realize this code is not exactly the essence of conciseness and brevity. > A "once" of a function is a use-once version of that function. Ie, > "once(func)" returns a object that will forward no more than one "run" > message to "func". The two argument form "once(verb, target)" is a > generalization which will forward no more than one "verb" message to > the target. > > For the Miranda Methods, the result of the once (the forwarder > below) must make good decisions about whether to override them and > possibly forward them, or not override them and let them default to > methods on the forwarder. For non-Miranda methods other than the > suppressed method, they are simply forwarded. > > def once { > to (verb, target) :any { > var used := false > def forwarder { > # use the Miranda order/3, though it shouldn't matter > > # use the Miranda optSealedDispatch/1 to protect the target > > # forward getAllegedType/0, though one could argue that, once > # used up, the type shouldn't include the supressed verb > to getAllegedType() :any { > target getAllegedType() > } > > # forward respondsTo, but supress verb. One could argue that res pondsTo > # and getAllegedType() should be consistent with each other. > to respondsTo(verb2, arity) :boolean { > verb != verb2 && target respondsTo(verb2, arity) > } > > # forward printOn/1 > to printOn(out) { target printOn(out) } > > # forward reactToLostClient > to reactToLostClient(problem) { > target reactToLostClient(problem) > } > > # use the Miranda whenMoreResolved/1 to protect the target > > # use the Miranda whenBroken/1 to protect the target > > # use the Miranda yourself/0 to protect the target > > # handle all other messages > match [verb2, args] { > if (verb == verb2) { > if (used) { > throw("used up") > } > used := true > } > E call(target, verb2, args) > } > } > } > > # default to suppressing "run" > to (target) :any { once("run", target) } > } what follows is not so much an explanation as a series of disconnected points that a bright and motivated reader might infer real knowledge from. point 1. I observe that type-systems work is very abstract and formal and if I were doing a type system for secure programming I would definitely look to the capability literature for conceptual guidance. too easy when doing formal work to lose sight of where the juicy "wins" (opportunities) lie and more generally to lose sight of the economic and social implications of the technical work and to start playing a sterile "glass bead game". insight and vision is where the capability literature is very fertile. here I'm speaking of the capability PL literature (much of which is ultimately based on Hewitt) not the older capability OS literature (eg Butler Lampson's paper from the early 1970s) which is all intertwined with hairy OS implementation issues and takes forever to learn, it seems to this languages geek. point 2. Alastair Reid writes: >> I now think the >> body of ideas around capability PLs (again mostly dynamically-typed >> OOPLs these days) is likely to be richer and more scientifically >> fertile for the long term than FP even. > >Can you say more about why you think OOP works better in this regard? >Is it because: >- the only way to act on them is via methods (I'm ignoring most > C++ features and public Java fields here) that is one of the things I like. on the E language list they say that certain languages have the AYCDISAM -- All You Can Do Is Send A Message -- property, which means you can always interpose a new object of arbitary behaviour between any two extant objects --a next level of modularity beyond the ADT. many capability PLs have the AYCDISAM property. the question comes up under AYCDISAM of how can you ever be sure you are talking to the real Bank of America (say) when there can be an arbitrary number of objects on the Network between you and the thing you think is the Bank of America object. note that simply asking a third object, eg, the Federal Reserve object, simply moves the problem. the solution is all elegant and subtle. in fact, ISTR it took bright folk years to figure out. "took years to figure out" is a big turn off to practical programmers, but to me, who would rather be a theoretical physicist than a programmer except programming is more economically important, it is a reccommendation when I can learn relatively few very subtle concepts (of the quality that they took years for a bright group to figure out) rather than many many many tedious uninspiring ungeneralizable details as in say most Linux software. point 3. I judge that it would be much easier (than say Linux) to be the system administrator of a complex "software environment" written to capability principles. you have more control over the environment because each individual software package (each of which is a kind of "guest of the system admin") has less control. for more see http://cap-lore.com/CapTheory/Politics.html point 4. the intellectual framework that underlies much of the capability PLs --Hewitt's Actors model -- is protean enough so that people have written articles that "redo" much of *physics* in Actors terminology and primitives. such protean-ness speaks well for fertility. in summary, I plan to keep on concentrating on the pure FP world because I calculate that it is more certain to gain (slowly: FP is not the Internet of 1993 by a long shot) in economic importance than the capability PL world is. the capability (PL and OS) stuff is either going to explode or remain obscure with obsure being the more likely fate next 6 years, and that makes for unreliable career planning. oh how cynical I have become! -- Richard Uhtenwoldt "It's a mammal thing; you wouldn't understand."

1 0

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

20 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 20 Aug '02

20 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