![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
if a variable can have many interface types (predicates? attribute types?), then need to decide at some point how much inference the compiler will do for you. right now i'm thinking that maybe CNF should be available but not DNF. So, for example, if you say that variable X is either of type A or B, and A implies Meters and Int, and B implies Meters and Float, then the compiler should allow you to pass X to something that demands an input of Meters -- that is, it performs inference to convert "(Meters and Int) or (Meters and Float)" to CNF form, namely, "Meters and (Int or Float)". And you could provide a case statement with "(Meters and Int) or (Meters and Float)", or a case statement with "(Int or Float)".
But not the reverse; when you provide a case statement on types, the compiler has to prove that your cases are exhausive, but if you say that X is either Meters or Feet, and then separately say that X is either Int or Float, then you cannot provide four cases ("(Meters and Int) or (Meters and Float) or (Feet and Float) or (Feet and Int)") -- the DNF of what is known about X is not computed. However, you could have a case statement with Meters or Feet, and then a nested case statement with Int or Float.
To give examples with more inference, you could say that X is "(Meters and Int) or (Meters and Float) or (Feet and Float)". Now you could have a case with "Meters or Feet", and in the Feet branch, you could assume it was Float.
--
so, the verification algorithm for verifying predicate P given known information X: if X is a conjunction, then for each conjunct C in X, search for syntactic matches of C (or weaker; so if C is "A or B", then "A or B or D" matches) in P (including subexpressions of P), and replace them with True (and simplify by removing the Trues, ie. "A and True" -> "A"). (to save time later, you might want to remove atomic conjuncts from X after doing this, assuming you won't expand some named type later and find one of those inside of it). if P becomes True, return Match
if P is atomic, and wasn't changed to True, return False
if P is a conjunction, then recursively test each conjunct, and return Match iff they all return Match
else, P must be a disjunction. return Match if, for any conjunct C of X (C must be a disjunction) (if X is a disjunction, then you have only one C, namely X itself), this returns Match:
test every disjunct Dx in C as follows, and return Match iff they all return Match:
if Dx is syntactically weaker than P (unnecessary; will be replaced in step 1 of recurse), or some disjunct of P (is that step neccessary? i guess not, for the same reason), return Match
o/w, recurse, matching Dx against Ptodo: add XORs, negation
some examples:
if you say X is "(Meters and Int and Red and Tall) or (Meters and Float and Red and Tall) or (Feet and Float and Red and Tall) or (Feet and Int and Blue and Tall)"
case on "Meters or Feet" and then if it's meters, can you assume it's Red? yes
case on "Red or Blue" and then if it's Red, case on "(Meters and Int and Tall) or (Meters and Float and Tall) or (Feet and Float and Tall)"
case on "Red or Blue" and then if it's Red, case on "(Meters and Int) or (Meters and Float) or (Feet and Float)", and then assume Tall
If you said X is "(Meters and Int and C) or (Meters and Float and D) or (Feet and Float or Red)", and C was "(Int and Red) or (Float and Blue)", and D was "(Float and Red) or (Int and Blue)", you cannot assume that X is Red, because you cannot express that Int and Float are mutually exclusive, because the system is monotonic (ppl also say "monotone"). or mb i should say "positive", b/c not only are the results of deductions in the system monotonic, but also all of the expressions comprehended by the system involve only positive literals.
for example, if you say X is "(Meters and ((Int and Red) or (Float and Red)) and Tall) or (Feet and ((Float and Red) or (Int and Blue)) and Tall)", then you can do
cases "(Tall and Red) or Feet" cases "Red or (Feet and ((Float and Red) or (Int and Blue)))" cases "Red or Blue" cases "Red or (Int and Blue)"
what you cant do is X = "(A or B) and (C or D)", cases "(A and C) or (A and D) or (B and C) or (B and D)"
the reason you cant do X = "(A or B) and (C or D)", cases P="(A and C) or (A and D) or (B and C) or (B and D)" is that the information from the different disjunctions in X (the two different conjuncts, that is) is never combined; the algorithm iterates over ["(A or B)", "(C or D)"] in the line "for any conjunct C of X". Each of the tests will fail, because "A or B" is not strong enough to imply P, and neither is "C or D". in other words, looking at this as algebraic simplification, "and" is never distributed over "or".
for the same reason, you cant do
X = "(A or C) and (A or D) and (B or C) and (B or D)" (cases) P = "(A and B) or (C and D)"
the reverse of both of these matches
however, note that if
X = "(Meters and ((Int and Red) or (Float and Red)) and Tall) or (Feet and ((Float and Red) or (Int and Blue)) and Tall)", then you can do P = "Meters or Feet"
then within the both case branches, you are permitted to assume Tall, and within the first branch, you may assume Red. This is because the compiler transparently propagates all assumptions back up to the case statement (or fn defn), and so effectively does
P = "(Meters and Tall and Red) or (Feet and Tall)"
perhaps that is misleading, tho? what if you did
X = "(Meters and ((Int and Red) or (Float and Red)) and Tall) or (Feet and ((Float and Red) or (Int and Blue)) and Tall)", then you can do P = "Red or Feet"
and then assumed Meters in the first branch? If this is transparently added to the condition, then things which are "Feet and Float and Red" will always go through the second branch, whereas just from looking at the case statement as written, it is ambiguous which branch these examples go thru (they match both conditions). i guess the easiest way to deal with this is to leave it "undefined" which branch of a case statement things go thru in case of ambiguity (i.e. when they fit the conditions for multiple branches).
but what about when someone wants to have a sort of case statement where instances go thru EVERY applicable branch, rather than ANY applicable branch? well, in that case, i guess you'd not automatically add other assumed things; the code in the branches of such a conditional should assume that the ONLY type information that can be assumed is what is in the conditional. but, anyway, the most common time when P will be a disjunct is not when there is an explicit case statement, but rather when some variable is required to be a member of a disjunctive type
(note that, in general, the facility for proving that case statements are exhaustive removes the need for defaults in such cases -- maybe a syntactic sugar transformation that transforms case statements without defaults into something else? all cases would have to be by type for this to work)
examples: cases "(Tall and Red) or Feet": P = (Tall and Red) or Feet X = "Tall and ((Red and (Int or Float)) or (Feet and ((Float and Red) or (Int and Blue))))"
P = Red or Feet X = "(Red and (Int or Float)) or (Feet and ((Float and Red) or (Int and Blue))"
dx1 = (Red and (Int or Float)) P = Red or Feet
dx1 = (Int or Float) P = True or Feet dx1 matches
dx2 = (Feet and ((Float and Red) or (Int and Blue)) P = Red or Feet
dx2 = (Float and Red) or (Int and Blue) P = Red or True dx2 matches
both disjuncts match, Match
cases "Red or (Feet and ((Float and Red) or (Int and Blue)))" P = Red or (Feet and ((Float and Red) or (Int and Blue))) X = Tall and ((Red and (Int or Float)) or (Feet and ((Float and Red) or (Int and Blue))))
P = Red or (Feet and ((Float and Red) or (Int and Blue))) X = (Red and (Int or Float)) or (Feet and ((Float and Red) or (Int and Blue)))
dx1 = Red and (Int or Float) P = Red or (Feet and ((Float and Red) or (Int and Blue)))
dx1 = Int or Float P = True or (Feet and ((Float and Red) or (Int and Blue))) dx1 matches
dx2 = Feet and ((Float and Red) or (Int and Blue)) P = Red or (Feet and ((Float and Red) or (Int and Blue)))
dx2 = (Float and Red) or (Int and Blue) P = Red or (True and ((Float and Red) or (Int and Blue)))
dx2 = (Float and Red) or (Int and Blue) P = Red or ((Float and Red) or (Int and Blue))
dx2 = (Float and Red) or (Int and Blue) {still in step 1} P = Red or True dx2 matches
both disjuncts match, Match
cases "Red or Blue" ? X = Tall and ((Red and (Int or Float)) or (Feet and ((Float and Red) or (Int and Blue)))) P = Red or Blue
X = (Red and (Int or Float)) or (Feet and ((Float and Red) or (Int and Blue))) P = Red or Blue
dx1 = Red and (Int or Float) P = Red or Blue
dx1 = Int or Float P = True or Blue dx 1 matches
dx2 = Feet and ((Float and Red) or (Int and Blue)) P = Red or Blue
dx2 = (Float and Red) or (Int and Blue) P = Red or Blue
dx2 = (Float and Red) or (Int and Blue) P = Red or Blue
dx21 = Float and Red P = Red or Blue
dx21 = (True) P = True or Blue dx21 matches
dx22 = Int and Blue P = Red or Blue dx22 matches
both disjuncts match, dx2 matches both disjuncts match, Match
cases "Red or (Int and Blue)" this'll work too -- it'll be the same as the previous until dx22, which will match P directly rather than one of its conjuncts matching
(note: we should not expand atoms until we get to them (or rather, until we get just above them; if we are in an OR, we must expand the atoms now in case they are ORs too, and then for those atoms which turn out to be conjuctions, we can leave them that way, for those that turn out to be ORs, we must expand each of their atomic disjuncts), and we should keep a running list of what has been set to True)
X = "(A and B) or (C and D)" (cases) P = "(A or C) and (A or D) and (B or C) and (B or D)"
matches
X = (A and C) or (A and D) or (B and C) or (B and D)" (cases) P="(A or B) and (C or D)"
matches
as per doug's idea, if something doesn't typecheck, optionally the compiler can run an NP-complete algorithm to try and make it typecheck (equivalently, compiler option to use NP-complete alg from the get-go)
each symbol in the program is associated with a node. the arcs from that node are various properties possessed by the symbol (e.g. the symbol possesses each of these properties simultaineously).
---
the type system must:
---
milewski's race-free type system:
http://bartoszmilewski.com/2009/05/21/unique_ptr-how-unique-is-it/ :
some type properties:
i believe the previous is a complete description of milewsky's system, (except for owner polymorphism, which i think can be done in a simple flexible way in Oot with annotations anyway), but should ask milewsky to be sure.
in oot:
additional operation: ':=', called "move": x := y == x = y; y = null;. The idea is that x gets the pointer and y doesn't have it anymore; this can be applied even to unique pointers, whereas normal =, which means copy, cannot.
you can declare a pointer with the type propery (other examples of type properties are , meaning "compiler, i demand that this cannot be mutated" and const, meaning)
his type system apparently provably avoids race condititions (both 'low level' and 'high level' race conditions, whatever that means). it does not prevent deadlocks.
"
Lessons learned from previous work
There are many commonalities in various approaches to race freedom.
Ownership should be built into the type system. In OO languages each object must have an owner. In C-like languages each piece of data must have an associated lock.
There should be efficient mechanisms for passing data between threads
By value
By reference. (The object being passed must be a monitor.)
As immutable data, by const reference
By unique reference using move semanticsMost of those ideas are expressible through type qualifiers. "
other sources: http://bartoszmilewski.com/2009/11/30/unique-objects/
http://bartoszmilewski.com/2009/09/22/ownership-systems-against-data-races/ http://bartoszmilewski.com/2009/06/15/race-free-multithreading-owner-polymorphism/ http://bartoszmilewski.com/2009/06/02/race-free-multithreading-ownership/ http://bartoszmilewski.com/2009/09/22/ownership-systems-against-data-races/
" The D programming language with my proposed race-free type system could dramatically improve the safety of message passing. Race-free type system distinguishes between various types of sharing and enforces synchronization when necessary. For instance, since an Actor would be shared between threads, it would have to be declared shared. All objects inside a shared actor, including the mailbox, would automatically inherit the shared property. A shared message queue inside the mailbox could only store value types, unique types with move semantics, or reference types that are either immutable or are monitors (provide their own synchronization). These are exactly the types of messages that may be safely passed between actors. Notice that this is more than is allowed in Erlang (value types only) or Kilim (unique types only), but doesn’t include “dangerous” types that even Scala accepts (not to mention Java or C++). "
---
note: i guess that in general, attributes that you want the type system to keep track of have a polarity; if they are absent, that says nothing about the system, but if they are present, some proposition is true. e.g. if a variable is immutable, that constrains something, but if it is not immutable, that constrains nothing.
however, sometimes you may need to assert that something is immutable, and sometimes you may need to assert that it is not immutable, right? not exactly... you can look at it as, sometimes (e.g. for milewski race-freedom) you need to prove that something is immutable. functions that mutate it in this viewpoint don't demand that it be mutable, they just mutate it and then the compiler infers that the immutability condition isn't true for that variable, and then the other part of the program, that demands immutability, doesn't compile.
and with structural typing, you might demand that something has such-and-such a member or supports such-and-such an operation, but you wouldn't ever need to demand that such-and-such a member is absent.
otoh immutable types cannot have a (usable) __set function. but i think we can neglect that level of expressiveness for tractability.
immutability and the like, then, are calcuated by specifying, for a basis set of primitive values, whether or not they are immutable, and then for every function, specifying upon which inputs/outputs some forbidden operation has occured. this idea also works for 'unique'.
e.g. for 'f(x) = y := x; y', where := is the move operator (i'd use ->), the compiler would infer, 'does not violate uniqueness for x; does not violate uniqueness for y', based on its knowledge that the primitive := does not violate the uniquness of either its input nor its output.
---
Not sure if the Oot type system has principal types. Apparently the ability to represent GADTs destroy principal types but i don't understand what they are: http://www.haskell.org/haskellwiki/GADT
Since we are more focused on types as a bag of unrelated properties, perhaps we dont have principal types. I'm not sure.
"class Eq a where " looks like a is a type parameter of Eq. (btw does haskell allow a destructuring bind on a in that statement?)
Hmm, the more i think about it, the more i think that we should ban type inference determining ad-hoc polymorphism which is polymorphic only in the return type (see [1] for more reasoning on that). This won't make the language any less powerful than, say, Python (in Python there is no type inferencing so in order to make an ad-hoc polymorphic choice, the class of the value that the object that you are dispatching on must differ (which would correspond to an input value in Haskell and probably in Oot). So i'm proposing that in Oot, you can have all the type inferencing you want, it's just that type inferencing won't be allowed to drive ad-hoc polymorphism from the "future" (from the types of the outputs).
Or, try THIS one on for size: the statically known (at the time of compiling the typeclass) kinds of the return types of different ad-hoc poly fns of the same inputs may not vary. Hmm.. but that sounds like you cant have two instances of the same kind of two different typeclasses. For example, it would prevent the empty homogeneous list from being both an empty list of ints and an empty list of fns, at different points in the program. No... it just prevents the existence of a fn, 'empty', that returns that. You can still have Int.empty and Fn.empty; or even, empty(Int) and empty(Fn). So, you can't have a single fn, 'empty', that sometimes returns statically known lists of ints and sometimes statically known lists of Fns, on the same inputs. This should prevent any type-level inductive hooey like Haskell's variadic fns, which uses the static knowledge of how many times the result of a fn will be applied in the future, which seems like a 'syntactic' thing, to alter the behavior of the function over the various applications. It still allows 'messages from the future', that is, it allows the compiler to automatically select among multiple instantiations of return-type-only-ad-hoc-polymorphic functions based on the expected return value, but it guarantees that all of the possibilities will be of the same kind (and kind incorporates the notion of 'syntactic' difference here)
but you could get around this by giving a dummy argument to the fun (empty(dummy)) so that the compiler can infer 'dummy' to be the desired return type
.
" Lets have two simple, small functions:
giveElements :: (a -> Bool) -> [[a?]] -> [[a?]] giveElements condition = filter (detectElement condition)
detectElement :: (a -> Bool) -> [a] -> Bool detectElement = any
The above seems a bit useless but I've extracted from it's surrounding code to show the problem. The 'giveElements' function is able to extract certain elements from a list and returns the filtered list. The 'detectElement' function does the job of deciding which elements are in and which are not. It does this by checking if any element of a list fulfills a certain condition.
So short so nice, but after some work on your program you discover that your 'condition' function required access to outside state to do it's job. Maybe the function has to do some a small modification of some data or should simply write a short message into a log. To allow this, you have to rewrite the above functions to use a monad. For this example lets simply use the IO monad here. Now the functions become:
giveElements :: (a -> IO Bool) -> [[a?]] -> IO [[a?]] giveElements condition = filterM (detectElement condition)
detectElement :: (a -> IO Bool) -> [a] -> IO Bool detectElement c els = do r <- mapM c els return $ or r
The first function still looks quite similar, only the 'filter' function is replaced by 'filterM' now. 'filterM' is the monadic version of filter and gives the monad back from the condition. So without filterM the state won't get up from the detectElement function (and of course there would be a type error).
detectElement looks a bit more different. The reason is that there is no monadic version for 'any'. So I use a monadic map (the mapM function) to create a list of Bools by applying the condition to each element and then check if at least one of the results it true. This doesn't requires more evaluations of c than the first version because of lazy evaluation, but it still required a complete rewrite of my code. It's still readable, but not as much as before.
...
And if you have more complex functions the above translation process from a non-monadic into a monadic-one is much more difficult and IMO it also destroy the clarity of the code. Also state monads have bad runtime characteristics because of their 'inside-out' evaluation which can fill up the stack quickly. You can use IORefs instead - but then you can't simply transform your program to using continuations anymore for example. And if you put a IO monad into a state-monad, you have to lift all IO-accessing functions via liftIO.
And whats the point of having a pure functional language, going thru lots of trouble to maintain the purity, only to get things like IORef which you tried to get rid of in the first place? If you design a program to use IO monads from the beginning everywhere, then you have fewer problem maintaining and expanding it - but then you're using Haskell like a normal imperative language. Whats the point of Haskell then? ...
Its not a problem of functional programming in itself, its a Haskell thing: While monads are quite powerful in principle IMO they are a pain to use in practice. Because monads show up in the return type of functions, the easy composition of functions which is the prime reason for the power of functional programming only works as long as all those functions use (compatible) monads, and sadly many functions simply don't exists in this form. "
hopefully Oot's attribute types will allow the monad-ness to be treated as orthogonal to everything else.
---
ok, whether or not we have principal types, i think languages to date have focused too much attention on them. Martin Odersky says http://www.codecommit.com/blog/scala/is-scala-not-functional-enough#comment-4162 "As to combining Hindley/Milner and subtyping: In principle it’s possible, but in practice it does not work so well. The problem is not so much that you end up too often with Any, but that inferred types become impractically large.". i'll have to look at scala to see what he came up with instead.
anyhow, my point is that some extant powerful type systems, like Haskell's, force the programmer to raise the level of abstraction but still to be very precise. You end up with long type expressions because of this. Also, you have to take all the facts about the type of an object and put them together into one long type expression, making sure that they are composed together in the proper fashion. For example, monads and monad transformers; the programmer things "this is a list of ints, and it is in the IO monad". To the programmer, these are two orthogonal pieces of information about the type of the object, but in the type system, one wraps around the other, and in a certain order (and it gets worse with monad transformers).
btw i'm sure someone has used the name "attribute types" before but it's probably something different from what i mean.
with attribute types, we never try to make the programmer interact with a single expression containing all the type information about a value (although they can query the compiler for that during debugging if they want). For example, this value is a list of something; this value is in the IO monad; this value is a list of ints. The programmer can look at either of these three as the type of the value in different contexts (note that the third implies the first).
---
in oot, what haskell calls 'existential types', which means expressions which dont completely determine a type, e.g. 'some type with a Show method' will be the rule, not the exception. this allows things like heterogenous lists. i think the usual problem with this is (esp. if you feed such a list through a function which reshapes it), then you lose the typing information on what individual items were, and all the type system knows is that they are elements of the heterogenous list, with only whatever properties are common to all items in that list. then how do you then polymorph on individual elements later?
e.g. if you construct a structure where you know that the first item in each list is a function reference, and all the rest of the items are integers, how do you get the type system to let you apply the function reference later? all it knows is that these are each members of a heterogenous list. i think the Right Thing for this case according to languages like Haskell is to create a data type (ADT) that specifically has a fn in one field and then a list of ints in another. But this imposes the type system on the programmer; in addition to the task of writing the program, they have the new task of explaining it to the compiler. And what if your knowledge about the structure of the list is hard to express; what if you know that the list is a valid AST for some language; do you want to translate the entire semantic grammar of that language to Haskell's type system?
in oot we want to make the task of explaining the program to the compiler optional. the 'promise' assertion will help here -- 'promise' tells the compiler to take something as a given (and to check it at runtime, unless runtime promise checks are disabled). This helps because you can tie promises to positions in code, rather than have them be universal truths about data types -- 'if we are here in the code, then you may assume this'. This saves you from having to construct a new data type for every state of knowledge that you have about your data (e.g. 'if this node of the AST is under a FOR-LOOP node, then the second child is an iteration variable symbol'), and from having to encode all your knowledge about the valid state transitions into the type system (e.g. an AST node of type AST-FOR-LOOP's second child is a node of type AST-UNDER-FOR-LOOP-ITERATION-VAR). Instead at the relevant point in your code you say 'we must be in an AST node corresponding to a for loop iteration symbol; i promise that this node is of type Symbol' This makes the program harder to reason about but easier to write, and even easier to read if the reader isn't an expert at the type system. It is equivalent to having weak typing/allowing unsafe type coercion like in C.
i think the other usual problem is, if you pass elements through a function that only demands an existential type, and creates new elements, you must distinguish between functions which guarantee to create new elements of the same type it was given, or functions which guarantee only that the new elements will satisfy the existential type.
---
i guess our type system would be described as
a type and effect system, optionally static, weak, inferred, structural (with optional nominal types)
---
in Haskell, existential types let you define a type which doesnt say 'this is a list of Ints', but rather, something like, 'this is a list of objects whose types are in the Show typeclass'. In Oot all types are existential because 'everything is an interface'; you describe the properties that a type in a certain slot has, e.e. the interfaces that types belong to, not the types themselves.
--
although it should not be mandatory to state which exceptions your code might throw (that's the compiler's job), it should be possible for a caller to insist that you throw only a subset of a given set of exceptions, and that anything else is a type error
--
--
could use Coq for type assertions and proving stuff about Oot programs, in the same way than Shen uses Prolog
see also http://adam.chlipala.net/cpdt/html/Intro.html , http://www.cis.upenn.edu/~bcpierce/sf/index.html
would eventually have to port Coq into Oot. note that Coq's not-Turing-completeness (via requiring 'obviously decreasing' structural recursion) is key.
--
hmm.. in addition to the restrictions contemplated above to prevent http://stackoverflow.com/questions/3467279/how-to-create-a-polyvariadic-haskell-function , might want to have more restrictions on global type inference than on local (see http://lambda-the-ultimate.org/node/2862 ).
--
the type system can be extended to detect 'taints' or 'untaints'. an untaint is the negation of a taint. a taint can be defined either as a whitelist (anything using only operations in the whitelist is untainted; anything built only from untainted operations is untainted; everything else is tainted) or a blacklist (anything using any operations in the blacklist is untainted; anything built only from tainted operations is tainted; everything else is untainted).
Note that the taint system has negation at the top (taint = not untaint) and at the bottom (the base case can be a whitelist or a blacklist), but that the bottom must be all one polarity or all the other, not both. This should simplify things by making it unable to express all boolean functions. I'm hoping that most of the type inference system can use positive logic, perhaps with a few extensions to deal with stuff like this.
note that the necessity of making a blacklist complete would require Oot to fix a set of primitive operations that everything is compiled to. An alternative is to first design the system to be fully expressive, but then to only support a published list of primitive properties that are guaranteed to be defined correctly (e.g. blacklisted if necessary) for every language primitive (e.g. stuff like side effect-less/side effect-ful, deterministic (the other part of referential transparency), reads, writes, moves, null). This achieves the goal of giving the language the right sort of machinery that can be repurposed to other tasks.
a taint can be calculated based on the operations used to produce a value (e.g. 'side-effect free' is an untaint of this sort; a function built out of side-effect free parts is side-effect free), or based on all operations applied to a VARIABLE (e.g. 'unique' is an untaint of this sort; the unique value could be 3 or it could be a function, but what matters is that if it ever read into another variable, then the original value is never used anymore; another one is 'const'). these two are related; e.g. if we want a variable containing a reference to be immutable, then we can only apply immutability-preserving ('const' in that variable) functions to it; but a const function if a taint of the first kind (defined inductively because a function that only applies const (in that variable) functions to that reference, and doesnt use any primitive mutation ops on it, is itself const).
we need ways to express: (a) a value or variable has the property (e.g. immutability) and (b) that an operation preserves or breaks the property (is whitelisted or blacklisted) (e.g. a function that does not write to a reference is 'const' in the D language, meaning it doesnt break the immutability)
perhaps this is not yet enough. We should be able to express D's transitive const (http://dlang.org/const-faq.html). We should be able to express Rust's pointer type system ( http://static.rust-lang.org/doc/tutorial.html#boxes-and-pointers ). We should be able to express [2].
---
swkane had a good idea that i summarized as:
" that's an interesting perspective that i hadn't considered; let the types stay complicated but try to find a way to make readable labels for them so you only have to dig into the complexity when you need to. "
--- http://www.haskell.org/haskellwiki/GADTs_for_dummies ( http://web.archive.org/web/20130702221947/http://www.haskell.org/haskellwiki/GADTs_for_dummies )brings up an excellent point: type classes are like arbitrary functions on types, with normal Haskell stuff like pattern matching, algebraic data types (multiple constructors), guards, etc, except with a confusing relational (rather than functional) syntax.
this brings up the obvious point: Oot could be like this but use normal syntax
seems like there is really a lot of mileage to be had just by delivering a uniform notation for data, code, patterns, types, typeclasses
--
remember that since type signatures are optional and principal types are not the core concept, you need a way to add type signatures to someone else's library code (without modifying their source code) ---
i guess maybe the reason why e.g. Haskell has an idiosyncractic syntax for typing is that they want to syntactically prohibit things they dont know how to automatically typecheck in a decidable, relatively complete way (relative to some nicely characterizable subset of dynamically valid programs)
GHC's typechecking algorithm has expanded over the years as progress was made
i guess i think it would be better to have a very simple, uniform syntax, assumptions, and compiler type errors that are simple enough to use in debugging, then allow for the case that sometimes the typechecker simply wont be up for the task, and the programmer must use assumptions to bridge the gap
--
see also PrincipalTypingConsideredHarmful?
--
the idea of unifying the type language and the normal language is discussed here:
http://lambda-the-ultimate.org/node/1085
some interesting pointers from that page to check up on later:
--
http://lambda-the-ultimate.org/classic/message6587.html#6615
--
book on the theory of coq:
http://www.amazon.com/kindle-store/dp/B000QCUCZU#reader_3642058809
interestingly this sort of asserts that Coq is the first real useful language that makes practical use of Curry-Howard:
http://lambda-the-ultimate.org/node/1532#comment-17865
"
Would it be possible to take an arbitrary mathematical theorem (let's say: "string concatenation is associative", or Fermat's little theorem) and express it as a type?
Yes, and in fact this is exactly what happens in automated theorem provers based around constructive type theory, or the calculus of (co-)inductive constructions. A good example of this is Coq. I would suggest reading through some of the tutorials/introductory documentation if you wish to learn more. Also, there is a good book on the topic (on Coq, Curry-Howard, and related issues): here. "
--
the roots of type theory lie in the effort to avoid things like Russell's paradox in the foundations of mathematics [see Stanford encyclopedia of philosophy]. The idea is to restrict the set of valid terms of a logic by putting type requirements on operators. You structure the requirements to prevent operators from applying to themselves or to things like themselves that can indirectly cause similar problems.
In some systems the way you know a term is invalid is that such a term has no type. The type system presents axioms and inference rules to make "type judegements" which assign types to terms, and if no type can be assigned to a term, it must be invalid. In this way the type system specifies a subset of otherwise acceptable terms.
For example, in simply typed lambda calculus, the predicate "lambda x . not[x x]", namely, the predicate of predicates that don't apply to themselves, has no type.
This semantics is problematic for Oot's notion of type attributes because the idea here is that we can have terms that we don't know much about; terms for which we have only partial information, or no information, about what type they are. For example, the Ootian approach to the above "bad" function would be either to say, "you can't apply a predicate to itself" [which still leaves open the door for more cleverly designed paradoxes], or to say, "i can't figure out the type of this and that's okay", again leaving the programmer to fend for themself against this sort of paradox.
e.g. if someone tried to define the function "lambda x: x x", oot would let them. Calling this function would cause an infinite loop, but so what?
Surely there is some way to finesse that sort of usage paradigm onto conventional type systems but this indicates that they may not be an appropriate basis for Oot. Especially because the whole original reason for their existence [e.g. to prevent Russell-ish paradoxes] is functionality that we are willing to do without. While we do want a logic to make type judegments on terms, we don't want to equate 'cannot be typed' with 'badly typed'. [Pierce's definitions still seems on-target, see Wikipedian defn quote]
otoh i guess we do want our type system to be consistent, even if we dont care about ruling out paradoxes in the object language, so we might need a little type theory just to ensure that. However, another approach would be to allow paradoxes and make our type logic paraconsistent, or something similar [e.g. is it paraconsistent to say that if we can derive both that x is of type t, and also that x is not of type t, that x is not of type t? i feel like there's some better way to phrase that :)]
remember also that perhaps the real challenge is that we want to allow the user to extend the type system. so even if what we provide is consistent, the user could add something inconsistent.
Also, recall that we want to allow the user to easily add things like "unique" [cannot copy] and "immutable" [cannot write to], as well as ownership types a la milewski [and wasn't there something else with a different form too, in terms of where the quantifier and where the 'not' was? todo]. Note that these are certainly over terms, not over base-level values [unless in our language all terms are values, like i guess in Haskell], as "unique" isn't really a property about what kind of value something is, rather it's about what operations you are allowed to apply to it.
it does seem as if there's one world in which you have functions applied to value objects like numbers, giving you values, and another in which you have terms being inductively generated and reduced by rewrite rules [implications], giving you something like grammars/proofs [methods which produce ever-larger sets of 'valid' terms by iteration]. Perhaps this second world is the pattern-matching/logic/type system part of Oot. But where does probabilistic logic fit in here? Here terms are not either derived or not derived, they are valued.
-- consider using sequents as the fundamental logical operation
---
took a very brief look at http://existentialtype.wordpress.com/2011/04/16/modules-matter-most/ and i agree:
" More disappointingly, for me at least, is that even relatively enlightened languages, such as Haskell or F#, fail to support this basic machinery. In Haskell you have type classes, which are unaccountably popular (perhaps because it’s the first thing many people learn). There are two fundamental problems with type classes. The first is that they insist that a type can implement a type class in exactly one way. For example, according to the philosophy of type classes, the integers can be ordered in precisely one way (the usual ordering), but obviously there are many orderings (say, by divisibility) of interest. The second is that they confound two separate issues: specifying how a type implements a type class and specifying when such a specification should be used during type inference. As a consequence, using type classes is, in Greg Morrisett’s term, like steering the Queen Mary: you have to get this hulking mass pointed in the right direction so that the inference mechanism resolves things the way you want it to. "
copied from elsewhere:
"
Lessons learned from previous work
There are many commonalities in various approaches to race freedom.
Ownership should be built into the type system. In OO languages each object must have an owner. In C-like languages each piece of data must have an associated lock.
There should be efficient mechanisms for passing data between threads
By value
By reference. (The object being passed must be a monitor.)
As immutable data, by const reference
By unique reference using move semanticsMost of those ideas are expressible through type qualifiers. "
btw the 'promise' vs. 'demand' thing w/r/t const vs. immutable and lent vs. unique (lent should be called noalias or somesuch) seems pretty common (wasn't this also the deal with Haskell's existentially quantified types or maybe with Haskell typeclasses vs. Java interfaces? or were those other things?). should have syntax for it, so you can just say 'i promise it will be immutable' and 'i demand it be immutable' without learning two keywords for each of these cases and remembering which one is which (or at least, have a keyword naming convention like promiseImmutable demandImmutable)
--- ...
hmm if patterns define types. thinking about logics for patterns. the usual tradeoff b/t expressiveness and feasible inference.
since type are in a hierarchy, this suggests descripition logics.
i feel like we can cut out negation somehow. but not quite sure..
some types, like 'immutable' or 'functionally pure', are 'purity' types, meaning that they are true whenever some condition of impurity never obtains in some transitive/data-flow-y manner.
others, such as Integer, are 'classy' types, defined as subsets of other classy types. in this case they aren't true unless you have a reason to believe that they are.
so it seems like you may want to write some notation and then put a 'not' in front of it. but you'll still never need a 'not' inside of it.
mb logics without negation are called "positive"?
i think the 'purity' types correspond to positive 'impurity' types, e.g. 'mutable', which we can use negation-as-failure semantics on, e.g. if you never any code that would mutate this value along the dataflow, you may consider it immutable.
description logics have negation, and are PSPACE-complete (at least as hard as NP-complete), so that's pretty hard (but hey, at least it's decidable) later: actually description logics EL and EL++ are polytime!
positive first-order logic is NP-complete (but hey, at least it's decidable) ( http://ecommons.library.cornell.edu/handle/1813/7017 First Order Predicate Logic Without Negation is NP-Complete by Kozen, Dexter)
do we really need both universal and existential quantifiers in our patterns, though?
hmmm... if there exists any mutation along the dataflow, then the variable must be mutable, so there's a there-exists. and a list of ints must contain all ints, so there's a for-all. but perhaps these are two different kinds of reasoning? e.g. it doesn't seem like you would ever need a forall if you are looking at a list of known types and trying to deduce new types, e.g. if the thing has type Int and type single-world-in-memory you don't need to look at both of those to deduce type Number, that's just a there-exists. similarly, you might want the type of a list of ints to say each element is an int, but you don't care about a list of things-with-at-least-one-int, so there you only need forall, not there-exists.
but just thinking about graph patterns, sure, sometimes you want to match a node which has at least one arc going to (Int or Real or Complex), and sometimes you want to match a node whose arcs all go to Int.
mb just that you can have either forall or thereexists but not both on one expression?
but what if you want to look at a list and see if it's a list of ints; you look at every item in the list (follow each arc), look at each of their types (follow the type arcs in the meta view), and then look for at least one of these type arcs to terminate at Int. But this is saying, forall arcs in the list, there exists a type arc from the target of the initial arc that targets Int. So we are mixing them.
we want OR; if something is an Int or a Float then it is a Number.
and i guess the last statement shows that we want Implies too?
could we possibly get rid of AND?
hmmm.. mb the two different activies above are, reasoning from the types to allowed values, vs. reasoning from program code to types.
e.g. reasoning from program code to types, we see that if there is a possible mutation, we must have type Mutable.
reasoning from the types to allowed values, we see that a list of ints must contain all ints
e.g. if you see a single non-int go into that list, then you deduce the impure type "non-list-of-ints", which is like Mutable.
similarly, from Immutable, you deduce that for every step in the dataflow, there is no mutation.
i think i may be conceptualizing this wrong. first off, for straight-up graph MATCHING, the problem is simple (this is like checking if an assignment to variables satisfies some set of FOL statements). the inference complexity comes when you are not presented with a single graph, but rather with a statement in this language (a statement about the type of the graph, i.e. a graph pattern), and you must deduce merely from that whether it will match another graph pattern, without reference to a single particular graph.
also, when i say that we want to deduce that because something is one type, it is another type, the types form a lattice. we can require the users to explicitly construct the rungs of this lattice, we don't have to infer them from the definitions of the types.
also, when i say that the compiler should infer if matching this graph pattern sufficies to show that that graph pattern will be matched, we can require a user to use the assertion facility to write a proof of this for us; the compiler is only checking the proof, not writing it. so if the problem of finding the proof is NP, then of course the problem of checking the proof is in P.
so mb it doesnt matter if theorem-proving in this logic is NP.
mb we just tell the programmer:
wait a minute... i think i am misunderstanding quantifier here.. we won't have statements like 'for all arcs a from node n, and for all arcs b from node n, a = b'. we'll have statements like 'for all arcs a from node n, let the target of the arc be m. for all arcs b from node m, ...'. we'll only quantify once at each level. so no, the quantifiers won't be exchanged. but used this way, this isn't really FOL quantifiers. we can't express things like 'for all arcs a from node n, there exists an arc b from node n such that b's label = a's label + 1'.
also, the reachability is like * is regexs, leading to the analogy that the reachability component of these patterns is like a regex over linear paths instead of over linear strings. a character in a string has a single successor but a node in a graph can have many (i.e. the outgoing arcs; or even the ingoing ones, i see no need to require the programmer to always respect directedness here, although that may be a good default, and some types of graphs may not permit the 'what links to here' query). so we need forall and thereexists to choose how to handle the multiple (Kant would say manifold) successors.
remember that we need to ask things about the reified edges, too, like what their label is
so i guess the type system will accept two kinds of definitive statements; "type A is a subset of type B" and "if something matches this pattern, then it is of type B". If you say "variable V is type B", then the system will enumerate all known types which are subsets of type B, and go through all known "if something matches this pattern, then it is of type T" for each such type T, looking for a match.
note: semantically, giving a pattern with "C or D" for type B is the same as saying "type C is a subset of type B" and "type D is a subset of type B". However, the system may not bother to infer this. (or will it? perhaps it should try replacing each type in the pattern with all of its subtypes..? or can we leave it up to the user to assert those things? no, if you have a type of 'list of numbers' and you assert that a list of Ints is of this type, that assertion should typecheck without you having to explicitly say it is a 'list of numbers' first. so it does try to match each type in the pattern against any subset of that type; but what it does not do is try to match the patterns of each of those subset types (because then we'd be recursing..). so if complex numbers are defined as things of the form (float, float), and you have a list like [(float, float), (float, float)], but you haven't asserted that the (float, float)s are complex numbers, then this list won't typecheck as a list of numbers ([Num]), because although it known that complex numbers are a type of number, it's not going to bother to match these patterns.
if you have a 'list of list of numbers', and you give it a list of list of ints, this should typecheck, but why? because it substitutes the 'list of numbers' match structure directly into the list match structure at the top. so it'll substitute in match structures of things directly mentioned, but not their subset types.
note: this way we never have to actually go into the 'type' metanode in our patterns for typechecking (except mb if we are doing something weird, not sure if we NEVER have to..)
how can we make the syntax for these patterns like [Num] for list of numbers? i guess that's just universal quantification. but mutability is existential..
with mutability: i guess it's important to be able to say that fns by default mutate unless we say they don't.. so we allow negations at both ends of the pattern (at the atomic elements, and at the top), just not in the middle.
hmm.. also should have an 'exactly one' operator (in addition to forall and exists), and an 'is-injective' operator (no two arcs have the same target), and a 'is-function' (no two arcs have the same label) operator.
hmm, now that we aren't doing inference, why not allow FOL anyways?
also remember we that we need a cons operator.. and i guess we need the analog of cons for graph nodes (i guess it's 'add this edge to this node') probably other more graph-y ones will arise.. the cons operator and its like must be able to appear on the left hand side of function definitions. Haskell used : and Shen used
| . |
also need parametric types; e.g. "swap(a,b)" of type A,B -> B,A where A, B are type variables
hmm.. principal types are too restrictive (since we want to uniformally treat type qualifiers such as 'unique'), but mb each node should only have one type when seen from each perspective?
@@ could refer to the last mentioned perspective (lexical scope), sort of an 'ibid' for Oot
mb -f means 'negation of f' (negation of True is False, negation of 3 is -3), and f- is 'inverse of f'
---
messages to handlers are a graph with a set of nodes distinguished as 'headers'. handlers match on any of the headers, and then get the graph, with that header as an entry point
---
another fundamental attribute of nodes is reverse arcs, that is, 'what links here'
---
http://www.shenlanguage.org/learn-shen/prolog.html
---
easy for loops like python enumerate
---
---
types:
there are three kinds of properties associated with types. one is propositions that hold true for every value of the type; these are things like "list of Ints". the second is propositions that hold true for every access of the value in the type; these are things like "unique" (seen as 'copy never applied to this'), "immutable". the third are things about how multiple accesses to the value relate to each other, or how access to this value relates to access to other values (this third definition is unsatisfactory because it is so general). included in this are things like 'unique' (seen as 'this variable's value cannot be changed without accessing it directly'), 'deterministic' (vs stochastic), 'no side effects', 'purely functional'.
a suitable notation for the first one need only use positive connectives, and possibly quantifiers, over values, with subtyping.
a suitable notation for the second one need only be expressed as marking each primitive operator with respect to the type, and then confirming that no negative primitive operator of the type is every applied to a variable containing the value (e.g. if you want it to be immutable, then no mutation is ever applied)
i don't know to capture the third one simply, since defining 'no side effects' seems to be impossible without a language for the semantics of the programming language. of course, 'no side effects' can be treated as the second case if we allow it as a primitive.
--- should name those. mb 'value types', 'expression purity types'.
---
types can have properties, e.g. conditions, and these can either be necessary or sufficient or both. necessary: every value of this type satisfies this condition, or in the second case above, every access to every value of this type satisfies this condition.
sufficient: if there is a value satisfying this condition, or if there is a variable whose accesses satisfy this condition, then it is of this type.
--- in fact, we should have a general notation that lets us write 'necessary', 'sufficient', and 'iff'
---
should we allow types whose semantics aren't fully defined, that is, ones for which a list of sufficient conditions is not provided? yes, because this is how we use the type system to attach arbitrary tags and qualifiers for use in metaprogramming.
---
note that we need to attach tags both to locations in the expression tree, and also to types.
mb ~ can be expression tree tags, not needing ^ also? or are footnotes different from arbitrary tags?
--
i guess if we use -> for logical implication then move should be :=
--
compiler/interpreter option to say if the necessary conditions of supertypes of the type of something are checked
--
'promise' has a different meaning for 'expression purity types' than its usual meaning; we are only promising that the expression purity holds within the function we are defining, not in general; but when we demand it, we demand it for all past and future, over all functions.
for value types, 'promise' has the usual meaning.
--
want a generic way to add modals and quantifiers to statements. 'promise' and 'demand' are modals.
mb should look at
http://en.wikipedia.org/wiki/Category:Logic_symbols
http://en.wikipedia.org/wiki/Modal_operator
interesting application of modal operators in http://en.wikipedia.org/w/index.php?title=Modal_operator&oldid=503040598
--
if Oot is general enough it should enable us to give commands that people would describe as rather philosophical, rather than practical computer programs that we know how to execute. E.g. the 'immortality program':
Search for a program whose semantics is extremely similar to the input-output relationships of the agent known as Eugene Baylis Shanks III, who has the attributes in the language English "human being born in Tennessee in 1979 C.E. on the planet Earth in this universe". If such a program is found, execute it.
This contains all sorts of complex ideas, all of which however are generic enough that Oot (or its std libs) could include them: search (without specifying how to carry out a search; e.g. looking for a program on the Internet or deterministically searching the space of all programs, or stochastically searching the space of all programs), a program, the semantics of a program, similarity, an agent, a name, the idea of attributes specified in a foreign language, a conditional on the result of search, the execution of a program.
note that placing the concepts of 'search' and 'similarity' in a std lib means giving Oot the ability to express ontologies (not necessarily baking a large ontology into Oot, however, although i think a bit of that would be a good idea also)
btw i used 'is' instead of 'are' on purpose because 'the semantics of a program' SHOULD be a similar concept.. perhaps as noted earlier, in this context 'semantics' is interchangable with the word 'meaning'..
---
end copied from elsewhere
---
"
Defining New Types
The real innovation in Qi is the use of sequent notation to define types. This is an enormously powerful means of defining types which gives Qi capacities beyond ML or even more recent languages such as Haskell. The use of sequent notation derives from Gerhard Gentzen who developed the sequent calculus treatment of first-order logic. In Gerhard's system a sequent is a pair composed of two lists of logical formulae called the antecedent and the succeedent respectively. The sequent is valid if the conjunction of the elements of the antecedent logically implies the disjunction of the elements of the consequent. The concept of logical implication is defined by laying down a series of sequent rules that say how sequents may be proved.
If the succeedent is restricted by only allowing one element in the list, then the system is a single-conclusion sequent calculus system; which is the kind that Qi is designed to represent. Qi requires that user-defined types be defined in terms of sequent rules. In other words, to define a type in Qi is to say how objects can be proved to belong to that type.
For instance, suppose we wish to define a type binary composed of all non-empty lists of 0s and 1s. Using sequent notation we would write:
if X e {0,1} X : zero-or-one;
This says that for any X, any sequent whose conclusion is X : zero-or-one (meaning X is of the type zero-or-one) is provable if the side-condition is satisfied (namely X is an element of the set {0, 1}). In Qi we writeif
(element? X [0 1]) : zero-or-one;
We state the simplest condition for being a binary number. Next we have two rules that say how bigger binary numbers are built out of smaller ones.
X : zero-or-one; [X] : binary;
\ binary_right \ X : zero-or-one; Y : binary; [X
| Y] : binary; |
\ binary_left \ X : zero-or-one, [Y
| Z] : binary >> P; |
| Z] : binary >> P; |
This says that if we have a list of at least two elements X and Y (followed by 0 or more elements Z), which is assumed to be binary, then we can replace this assumption by the assumption that [Y
| Z] is binary and X : zero-or-one. We need both rules because the first rule says how to prove conclusions of the form .... : binary and the second tells us what we can infer from assumptions of the form .... : binary. |
Here is a script showing the definition of the datatype binary as a non-empty list of 1s and 0s.The function complement calculates the complement of a binary number. Notice there are no special constructor functions for binary numbers - we just use lists of zeros and ones in a natural way. But this means that there is no obvious way of telling if [1 1 1 0] is intended to be a list of binary numbers or a list of numbers. To avoid headaches and combinatorial problems in typechecking, Qi insists on the explicit typing of functions.
" -- http://www.lambdassociates.org/qilisp.htm
--- maybe instead of outside-the-system sequents (that let you define new logics e.g. substructural logic), we should use classical logic and restrict the programmer to defining implication-like things in sequent form.
e.g. "A and B and C -> D or E or F"
but not e.g. modus ponens, which is built in to classical logic
otoh would be nice to have a uniform notation for nonclassical logics..
--- 18
" @9:
If a function mutates local variables, but does not mutate global state, for all practical purposes it is just as good as a stateless function. From the callers perspective it is stateless.
Indeed, and Haskell's type system is rich enough to express this constraint. See http://www.haskell.org/haskellwiki/Monad/ST#A_few_simple_examples
Posted by: Dan
| November 10, 2009 7:41 PM |
" -- http://scienceblogs.com/goodmath/2009/11/philosophizing_about_programmi.php#comment-2064185
me: yes, but... the other guy's point is that having to use the ST monad for that isn't quite as convenient.
toread: http://cs.anu.edu.au/~Ben.Lippmeier/project/thesis/thesis-lippmeier-sub.pdf
---
decidable dependent types stuff:
Dependent types are based on the idea of using scalars or values to more precisely describe the type of some other value. For example, "matrix(3,3)" might be the type of a 3×3 matrix. We can then define typing rules such as the following rule for matrix multiplication:
matrix_multiply : matrix(k,m) × matrix(m,n) matrix(k,n)
where k, m, n are arbitrary positive integer values. A variant of ML called Dependent ML has been created based on this type system, but because type-checking conventional dependent types is undecidable, not all programs using them can be type-checked without some kind of limitations. Dependent ML limits the sort of equality it can decide to Presburger arithmetic; other languages such as Epigram make the value of all expressions in the language decidable so that type checking can be decidable, ...
http://www.cs.nott.ac.uk/~txa/publ/ott-conf.pdf Observational Type Theory (epigram 2)
http://en.wikipedia.org/wiki/Intuitionistic_type_theory something to do with Epigram
http://en.wikipedia.org/wiki/ATS_%28programming_language%29 supercedes Dependent ML
ATS also has the good idea of token prefixes which indicate boxed or unboxed types
---
---
SAGE has an interesting idea: "hybrid type checking":
"Sage performs hybrid type checking of these specifications, proving or refuting as much as possible statically, and inserting runtime checks otherwise."
---
perl's notion of grammatical modes, i.e. context-dependence, is interesting, but i don't think that, e.g. plurality (scalar or list context), is a good choice of mode. in natural languages, we have plurality and gender and case and ?what else for nouns, and (conjugation), tense, aspect, mood, evidentiality, ?what else. more generally, in natural languages we have parts of speech: nouns, verbs, prepositions, adjectives, pronouns, adverbs, conjunctions, and interjections (see http://en.wikipedia.org/wiki/Part_of_speech for more). kant provides a system of "categories", or (hyper)logical modes ("hyper" if logic is taken to be merely boolean or first-order logic, since Kant's system is more expressive than these). anyhow, the "best" grammatical modes for programming languages are probably different than these (we don't seem to need gender, for example, although who knows, mb a clever use of gender could make it easier to read complex nested expressions... hmm, i think that's actually a good idea, todo...).
why have conjugation/declension? not for matching, as in natural language (but see the idea above about using "gender" to write expressions with less parens..). but for power/reuse
perl also makes the mistake of having similar-seeming operators that have different coerced types (i.e. == is numeric context, eq is string context). unless the morphology of the operator makes it very clear what type it is, this is confusing. also, it does the reverse of what you want in programming languages (to use modality for power/reuse); here we have one "conceptual" operation with many different lexical realizations; what we want is one lexical realization per conceptual operation, with modifiers.
here are some ideas for "grammatical modes" that might be good for programming languages:
default type (perl has numeric, boolean, string; but i dont think this works too well, at least compared to alternatives like explicit coercion, implicit coercion, python protocols, or haskelltypeclasses) vectorize quoted referenced (meta-level?) ignored concurrent assertion boxed/wrapped declarative/logical statement/constraint variable (comment; in parens b/c i consider this to be at a lower level than the actual programming language) (literal; in parens for the same reason as comment) purity access permission scope header/declaration/vardecl vs body transaction (todo: generalize) maximization polarity (positive vs. negative, max vs min, true vs false; or tripolarity (t/f/maybe, +/-/neutral, etc) (mb generalize to n-ary arity? mb generalize to algebra, include things like the wu xing?)
a clean mapping from noun->data and verb->function may not be the best. because in the semantics of natural language, nouns are state, yes, but verbs have lots to do with time. now, a pure computation has no relation with time (it is beyond, or before, time). but an impure computation with I/O side effects does have to do with time. this suggests that pure computations should all be nouns, and impure should be verbs. but whether a computation is pure or impure depends on how you define which bits of state are "inside" the system; a computer can mutate purely internal variables without becoming impure, but if it mutates (or reads) external variables, it becomes impure (monads have to do with defining which state is in the system). so the question of whether a variable read (or write) is pure or impure is context-dependent. but whether a word is a noun or verb is not (very) context-dependent. so this questions requires further thought (todo).
keyword arguments are like adverbs/adjectives
note: i like perl's "it" pronoun ($_), but if you let "print" be a shortcut for "print $_", you need to have another way to pass "print", the function. which is fine. oot's version of $_ should have lexical scope by default, unlike Perl.
todo: read http://www.google.com/search?q=haskell+open+data+paper&ie=utf-8&oe=utf-8&aq=t&rls=org.mozilla:en-US:unofficial&client=iceweasel-a , including SYB3, and Open Data Types and Open Functions
search for attribute typing, attributive typing, attribute type system, attributive type system, partial typing, partial type system
property typing, property type system
predicate typing, predicate type system
propositional typing, propositional type system
fractional typing, fractional type system
--
success typings
toread
http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf
also contains a related constraint propagation alg
mb also read later pubs by the same ppl:
http://user.it.uu.se/~tobiasl/publications/contracts.pdf
they implemented this stuff in a tool for Erlang, http://www.erlang.org/doc/apps/dialyzer/dialyzer_chapter.html
discussion:
http://lambda-the-ultimate.org/node/1910 http://www.quora.com/Has-anyone-used-success-typing-to-infer-and-validate-types-in-Python
also, a paper extending this work with a better algorithm that gives readable errors:
http://users.dsic.upv.es/~jsilva/papers/PEPM2013.pdf
related thesis: http://artemis-new.cslab.ece.ntua.gr:8080/jspui/bitstream/123456789/5300/1/DT2010-0190.pdf
an extension to catch more errors in certain cases:
http://hopa.cs.rhul.ac.uk/files/submissions/hopa2013_submission_7.pdf
currently cited by 48 articles in google scholar (http://scholar.google.com/scholar?cites=5054461946260377911&as_sdt=2005&sciodt=0,5&hl=en ), including this one which mentions success typings:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.4627
Static Detection of Race Conditions in Erlang : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.5681
this much-cited paper on TypeScript? claims that Success Typings are similar to the framework they use, called "abstract interpretation": (later: i don't know why i wrote that this paper is related to typescript; maybe whatever link i found it via said that? or maybe i confused Anders Møller and Anders Hejlsberg and Erik Meijer?)
http://cs.au.dk/~amoeller/papers/tajs/paper.pdf
--
so mb what we need is just for each term to keep track of (a) a set such that if the term has an attribute within this set of type attrs, it definitely is ok, (b) a set such that if the term does not have an attr within this set of types, it definitely fails. do we also need the negations, e.g. attributes such that if it has them it fails and if it doesnt, it succeeds? do we also need to explicitly keep track of promise vs. demand?
--
my hunch, not fully developed, is that we'll end up needed just
(a) a set such that if the term has an attribute within this set of type attrs, it definitely is ok, (PERMITTED, or P)
(b) a set such that if the term does not have an attr within this set of type attrs, it definitely fails. (OBLIGATIORY, or B)
by adding their own custom type attributes and logic to go with them (see http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf for an example of the form of such a logic; i havent read it yet but it looks like sequent calculus will do the trick), the user can extend these to be more expressive.
for the default, we'll choose readable and tractable over expressive.
my hunch is that it will suffice for one of (a) or (b) to be CNF and the other to be DNF.
for example, let's say that you see
f(x) = 3
we start by looking at 3 and saying, P = B = {3}, and looking at x and saying:
P = {}, B = {*}
now we look at f(x) and we say,
f: t(x) -> t(3)
therefore P(f) = B(x) -> P(3), so P(f) = * -> {3} and B(f) = P(x) -> B(3), so B(f) = {} -> {3}
umm... not quite.. the reasoning has to go both ways at once.. also, why is the literal 3 appearing as the type?
hmm for the both ways. if a value is being consumed as the input to a function, then that value's B is like offers, P is like hmm.
so,
P(3), B(3) = {3}, {3} P(x), B(x) = ?,?
actually i think both P and B (the strict typing and the 'success typing') must be INTERSECTED ("unified") at each step. that is, they go in the same direction. the difference is that when there are multiple branches of control flow, the P is pessimistic and the B is optimistic. e.g. in the http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf paper, they make a point of noting that in Fig. 2, Derivation rules, APP, that usually APP would say that the type assigned to an application of a function would be a subset of the function's range, but in their system its a superset. i see also that there CASE derivation rule takes the OR of the cases, i assume this is also unusual and due to the liberality of success types.
--
toread++ http://people.fas.harvard.edu/~lib153/lectures/typechecking.pdf
-- good slides on Disciple (DDC) haskell variant:
http://cs.anu.edu.au/people/Ben.Lippmeier/project/disciple/disciple-anu-2008-06.pdf
these slides talk about Disciple' effect and region typing. Disciple seems like it might be a good language to implement Oot in, but it's not as mature as Haskell.
i agree with disciple about how you should use something like effect types instead of monads. however, i think oot attribute typing is a more general, uniform solution to this sort of thing.
--
Disciple (which is strict by default) has interesting syntax for laziness: f x is strict, f @ x is lazy
--
Disciple has effect, region, and closure typing. i dont understand the latter two.
--
http://cs.anu.edu.au/people/Ben.Lippmeier/talks/poisoning-20090618.pdf brings up an important problem he calls "poisoning":
if "mutable" is part of your types, and if "pi" is immutable, then using traditional type inference, if you have:
x = x + 1 if blah then x else pi
then you'll want to say that pi must be mutable (because x is clearly mutable; and you'll say that both branches of the if have the same type).
--
what i think oot should do about poisoning is to allow the if to have the disjunctive type (union sum type, i think they call it) of the branches of the if.
and i guess if you have type information about multiple attributes (multiple type 'dimensions' you could call it) then that's a conjunctive type (product type, i think they call it)
---
chapter 3 explains the challenges of typing Python (stemming mainly from dynamicity):
http://web.archive.org/web/20081209222213/http://www.ocf.berkeley.edu/~bac/thesis.pdf
http://www.quora.com/Has-anyone-used-success-typing-to-infer-and-validate-types-in-Python
