proj-oot-ootTypeNotes4

interestingly, Curtis Guy Yarvin of Nock and Hoon and Urbit fame came to the same conclusion that i did w/r/t the difficulty of backwards inference in Haskell et al's type inference: http://www.urbit.org/2013/11/19/urbit-is-easy-ch10.html

also, the Golang folks came to a similar conclusion regarding everything-is-an-interface, although i wish to pursue that even further than they.

--

python's built-in types: http://docs.python.org/3/library/stdtypes.html

see also http://docs.python.org/3/library/types.html#standard-interpreter-types

rpython's types: http://doc.pypy.org/en/latest/rtyper.html

--

idea from Hoon: "The general principle is that name resolution across a fork works if, and only if, the names resolve to the same axis on both branches." i.e. that's somewhat similar to saying that if you have a value whose type is a (structural) union type, you can access a part of the structure iff the structure in the structure tree 'above' that part is identical in all types in the union

--

GTD/todo.txt @contexts vs. +tags; there is only one @context at a time (modal), used for filtering todo items to a sublist apropos to this context

relevant to type systems?

--

As Joel, I and a number of

As Joel, I and a number of others discussed on #haskell, part of the problem is that haskell's type system is poor at typing the kinds of things he was doing. For example, given n message types and m entities accepting o combinations of message types, there is no good solution for typing this accurately while retaining pattern-matching even with GHC's extensions - it can be done, but at the cost of much unboxing and reboxing and a type syntax that requires an indirection (or a good coding convention) to figure out which message types're actually accepted. By Philippa Cowderoy at Tue, 2006-01-24 01:44

I'd like to hear more about
login or register to post comments

I'd like to hear more about this - I don't really understand the issue with static typing, particularly since Haskell infers types. What was wrong with the general "data Event = ..." approach, with one constructor for each event type sent? It seems like an Erlang tagged tuple directly corresponds to a Haskell algebraic type (the tag atom is the constructor, and then the other elements are the arguments). Does Joel go into this any more in-depth anywhere? By Jonathan Tang at Tue, 2006-01-24 03:28

What's wrong is that it
login or register to post comments

What's wrong is that it gains you little more than dynamic typing does. You know you've got an event, but you've no clue if it's one of the ones you handle. By Philippa Cowderoy at Tue, 2006-01-24 15:03

login or register to post comments

--

...

I second your point about the robustness of the resulting Haskell code. I said in some other post that if it builds then it's probably right. My pet peeve, though, is that Haskell seduces you into coding for clarity and beauty. Haskell seduces you into coding the natural way. The natural way is concise since you can let type inference do the work, use lists, etc.

Then reality kicks in and you realize that the code is not running fast enough or consumes gobs of memory or spends 70% of its time collecting garbage. That's when you start putting strictness annotations all over the place unrolling your lets into cases and so on. It gets ugly.

Now, there are masters out there like Oleg Kiselev (Zipper OS) or Simon Marlow who probably don't have any trouble at all writing code that's both concise, beautiful and fast. I'm not one of them, not with Haskell. I find that doing things the natural way in Erlang hides no surprises and runs reasonably fast. Same thing about Scheme as I just set out to prove. By Joel Reymont at Tue, 2006-01-24 01:47

login or register to post comments

--

conjuctions and atomic negations only? or negations only in dataflow?

in more detail, we may want to restrict the logical operations that can be used to create new types out of combining existing types to make type inference tractable. Ie we could permit the creation of a type that says "X is of type A iff X is not of type B" but also permit "X is of type D iff X is of type B and X is also of type C" and also "X is of type E if X is of type B, or if X is of type C". But without further constraints elsewhere, that would make inference intractable in the general case.

so, some obvious constraints in this area are:

or, as noted above, we could leave this unconstrained and put constraints elsewhere

---

todo read:

http://www.q-lang.io/

---

don't make these mistakes with generics and their implementation:

http://nomothetis.svbtle.com/smashing-swift

three issues:

---

related to the previous:

"

noobermin 1 day ago

link

Just to point out, the last two sound like it's due to the current implementation (compiler) being new, so it isn't so upsetting at all.

Now, not supporting functors is odd, though.

reply

...

And yes, we should expect it as "normal" for new languages, because it is what people have come to expect to have available - although some implementations leave a lot to be desired.

If we consider how C# implements Functors for example, we see that it requires special language support, where the compiler essentially pattern matches over your code, looking for a method named "Select", with a specific signature taking a generic type and a func. This implementation completely misses the point that Functors themselves, while useful, are not special - they are a specialization of a more general concept we have - typeclasses and higher-kinded polymorphism. C# also adds the ability to create Monads, Foldable, Comonads etc, using similar patterns - but you can't create your own typeclasses, and are left to the language designers to add a desired feature.

The decision to add them onto C# like this was made not without knowledge of this, but out of consideration of working with the existing language, which was designed without their consideration, hence, why they're a pretty ugly design compared to the simplicity of Haskell's implementation.

[1]:http://www.cs.tufts.edu/comp/150GIT/archive/mark-jones/fpca9... [2]:http://research.microsoft.com/en-us/um/people/simonpj/papers...

reply "

---

hoon has a good idea:

orthogonal odor and size (generalize the addition of orthogonal size to type attributes)

(but in addition to the ortho 'size', having the 'odor' for atoms plus also structural typing sounds good)

--

the hoon tutorial explains typing as being motivated as a way to access nodes in by name instead of number

---

making the type syntax mirror/the same as the normal syntax:

http://www.haskell.org/haskellwiki/GADTs_for_dummies

---

http://blog.getprismatic.com/schema-for-clojurescript-data-shape-declaration-and-validation/

---

http://blog.cognitect.com/blog/2014/7/22/transit

---

support for 'laws' e.g. Haskell's 'monad laws'. then need to also support 'theorems'. combined with the support for homomorphisms, and for this should allow us to represent mathematics in the type system (although not necessarily to automatically deduce theorems about such things)

--

the idea of haskell data constructors as a type-within-a-type (note that in Haskell implementations, 'dynamic pointer tagging' refers to tagging objects with (a) whether they are already evaluated, and (b) which constructor they are within their type, not to which type they are, because being static thec Haskell compiler has already type-checked that) is interesting and possibly a fundamental way to generalize/simplify. So now we seem to have at least 3 types of types: atomic types (Hoon's odors), composite types (C structs, Python objects, Python and Haskell and Lisp lists, Python dicts, Hoon's structural typing), and the choice of data constructor within a Haskell type (eg is this List a Cons or a NilList?? is this Maybe a Nothing or a Just?) in addition, there are interface types vs representation types, which may be an orthogonal axis

---

java apparently has some sort of pluggable type system via annotations:

http://docs.oracle.com/javase/tutorial/java/annotations/type_annotations.html

---

note that now that we see the need for multiple orthogonal 'views' to be attached to a data value at one time, does this unity views in some way with type attributes?

---

faceted classification: for each (view?) facet, we have a separate suclass relation

---

" ahejlsberg commented on Oct 4

This is the starting implementation of Union Types as proposed in #805. It includes all parts of the core proposal, but not the "Possible Next Steps" (yet). The implementation reflects the decisions we made in the 10/3 design meeting.

@RyanCavanaugh? The pull request doesn't yet include new test baselines (and thus the Travis build will appear to fail). The deltas all look good, but a number of tests are now incorrect and need to be modified. I'm wondering if I can get you to help out with that. Anders Hejlsberg Initial implementation of Union Types e836fe1 CyrusNajmabadi? CyrusNajmabadi? commented on the diff on Oct 4 View full changes src/compiler/parser.ts @@ -1739,6 +1741,22 @@ module ts { return type; } + function parseType(): TypeNode? { CyrusNajmabadi? Collaborator CyrusNajmabadi? added a note on Oct 4

right now it looks like it's not possible to have syntax for an array of union types. That seems like it could be problematic in the future. For example, say you have htis in your .js:

function foo(x: string

number) {
    return [x];}

This function will have a type that is nonexpressable with the syntax of the language (and thus would be a problem for .d.ts files, as well as anyone who wants to explicitly give typings to things). Ryan Cavanaugh Collaborator RyanCavanaugh? added a note on Oct 4

We can write this as Array<string

CyrusNajmabadi? Collaborator CyrusNajmabadi? added a note 27 days ago
number>

Great point. We'll likely have to do that if we don't make additional syntax. As htis is a perfectly reasonable workaround, i'd prefer this approach before adding more syntax. thanks! Doug drubino added a note 16 hours ago

It would be great to have union type aliases, to keep the length of type names managable:

define number

Array<number>Matrix<number> = DynamicMatrix?;

Other values for the define keyword could be alias, type or class Doug drubino added a note 16 hours ago

I imagine this will fall out as a default feature, based on the type inference system of TypeScript?, but I think it bears repeating. Union types should have anonymous interfaces:

class A { commonToBoth: string; uniqueToA: string; }

class B { commonToBoth: string; uniqueToB: string; }

var either: A

B = new A();

Valid because there is an anonymous interface containing the common members either.commonToBoth

The anonymous interface would have the form:

interface `unnamable { commonToBoth: string; }

Or go wild and give this interface a name like:

Intersection[A

Common[A Interface[A Infc[A
B]
B]
B] or
B] for brevity

This does not have any use case I can think of, but perhaps I'm not thinking hard enough.

@DanielRosenwasser? Yes I do. So consider this an upvote. =) Daniel Rosenwasser Collaborator DanielRosenwasser? added a note 16 hours ago

@drubino you mean like in #957? :smiley:

This is a relatively old conversation at this point - you'll find quite a bit has happened recently with respect to union types, such as #914. Doug drubino added a note 16 hours ago

Haskell has union types denoted by Either A B. From conversations with members of the Haskell community, I've heard that this feature causes a lot of switch statements, leading to verbose, branching code. I'm not sure how to handle this, but perhaps one could create implicit type checks and blocks that use the order of the types as their listed on the union type. This keeps the syntax light-weight.

Something like:

var x = A

for x do { /Handle A } or { /Handle B } or { Handle c }
B C;

When combined with the anonymous interface idea, along with syntax to combine or skip blocks if logic can be implemented by common members in certain cases, you might be able enable the user to be quite succinct for common scenarios. Doug drubino added a note 15 hours ago

It might also be interesting to have a way of defining union types. Perhaps there is one master type that all others can be cast to, and the cast is specified in the definition. The compiler would then handle optimizations where casting can be proven to be unnecessary:

class DynamicMatrix? contains number

Array<number>Matrix<number> {
     super: Matrix<number>
     (x: number): Array<number> =  x => [x];
     (x: Array<number>): Matrix<number> = x => new Matrix([x]);
     (x: Array<number>): number = x => x[0] 
         when x.length === 1
         otherwise throw 'Array to number conversion is not possible';
     (x: Matrix<number>): Array<number> = x => x[0] 
          when x.numberOfRows  = 1
          otherwise throw 'Matrix to Array conversion is not possible';}

This is probably a bit more complex than the design team had in mind for union types, but I thought I'd throw it out there all the same.

I believe this, or features like it, would provide us with language constructs that would help to bridge the gap between dynamically typed languages and statically typed ones.

" -- https://github.com/Microsoft/TypeScript/pull/824

---

a comment on HackerNews? inspires an argument against a language providing only the tools to build a type system (one of my ideas), rather than a good base type system plus extensibility:

" "One can of course say, "Oh, send only messages. We are all adults here. Let's just agree to be nice. Stop sharing mutable memory between goroutines!" But all it takes is "that guy" or "that library", doing it "that one time" and then there are crashes during a customer demo or during some critical mission. It crashes and then good luck trying to reproduce it. Setting watchpoints in gdb (or the equivalent Go tool), asking customers "Can you tell me exactly what you did that day. Think harder!" and so on." " -- https://news.ycombinator.com/item?id=8575755

in other words, if the language provides a static type system, then you can use libraries and securely assume that whatever sorts of bugs the language-provided type system eliminates, those kind of bugs won't be present in the libraries. If the type system eliminates many sorts of bugs, then the library ecosystem will be less buggy.

by contrast, if the language only provides the tools for constructing a type system without providing an actual type system, then some libraries will use strong type systems and others will use weak type systems, and the robustness of libraries will be more variable

---

in the context of oot, the argument in the previous entry is already closed, b/c i have already decided that we want gradual typing.

however, maybe we could have a 'taint' system to make ppl very aware of when they are using a library that isn't strictly typechecked.


good example/food for thought about type system complexity:

http://stackoverflow.com/questions/1722726/is-the-scala-2-8-collections-library-a-case-of-the-longest-suicide-note-in-hist

---

usually the program only provides hints about which specific representation data type it wants, but i guess sometimes a specific representation data type may be mandatory (i think i had an example last night, but today i can't think of it though); in this case we might want to use the ! sigil

---

! to demand a specific representation, rather than request

---

"make illegal states unrepresentable" -- Yaron Minsky

---

today i woke up with the phrase 'manifestly bound theorems' in my head. This doesnt seem to be on the internet. Neither does "manifest binding", so i guess i made it up. Can we think of a cool meaning?

How about, "theorems who only apply for a given segment of source code and such that the relevant source code is explicitly labeled as such"? That is, having explicit labels in source code whose sole purpose is to be referenced by the theorem (because the labels say the region of source code where the theorem applies)

i guess an obvious example would be a theorem proving a loop invariant, which is bound to the region of the loop.

type inference and typechecking is also a theorem.

and i guess these (typechecking and theorem-proving) go together if we want our extensible typechecking to do stuff like in Rust.

but if that's what is meant, why not just call them 'scoped theorems'?

i guess a better name is 'region labels': naming a (static) region of code rather than just a specific point in code note: the regions dont have to be a (potential) scope to be labeled, eg begin-label-a if x then {y1; end-label-a; y2; y3;} else {z1; z2; z3; end-label-a;} point invariant: a proposition that holds whenever a specific point in code is reached region invaraint: a proposition that holds whenever any point in the region is reached

(note: what i am calling a '(potential) scope' in the previous paragraph is like the biological concept of a 'clade'; it is a region that includes all and only the descendents of some single node)

theorems can then themselves be 'scoped' to regions, meaning that they can assume things that are only true in that region, and their conclusions may only apply in that region.

also, preconditions/postconditions (like eiffel's require/ensure: https://www.eiffel.com/values/design-by-contract/introduction/ ) a contract (or perhaps also theorem, in cases where it is proven) where assumptions are made at one border of a regions, and promises contingent upon those assumptions are given at another point

(notice the modal demand/promise operator; note that modal logic here just being like the mode bits in Oot Assembly Notes 4 syntax!)

---

i think this is a key (if 'obvious') insight, but i'm not sure enough yet to promote it to the 'ootTypethoughts' page:

generic types are functions (type variable means a fn is involed), and typeclasses are types of types

note dynamic logic also generalized modal operators in this way (in passing) (to review, in dynamic logic, we create model operators to make statements of the form "if action A is taken, the proposition P will be true", written "<A>P". <x> is therefore a modal operator with a variable in it. We might have written it "<>_x")

so a generalization is to replace a constant by a variable (creating a fn), and then introducing types for this variable

anything 'with a variable in it' is a function; you 'call' a function by substitution, yielding an expression for the result, which then must be reduced

---

imo covariant and contravariant are most easily understood in terms of the Liskov substitution principal combined with pre- and post- conditions; a subclass can weaken the precondition and strengthen the postcondition; input types are preconditions and output type post-; so input type are contravariant and output types covariant. in some cases it should be possible to isolate a co- or contra- variant subset from an invariant interface, eg freeze an array and make it readonly for covariance by only exposing those functions that don't take any inputs of the parameterized type

---

'implementations' can be native (implemented in native code), or not. Implementations can have dependencies on other implementations. Note that, although implementation code inheritance is one type of dependency, that this is different from subtyping (these two things are confuted in traditional OOP, in which subtyping is confuted with 'class inheritance').

Type subtyping in Oot applies to types (interfaces), not to implementations; they are like (some kinds of) typeclass Contexts in Haskell. Eg any thing that supports the Float type also supports the Number type; anything that supports the Ord type also supports the Eq type.

Another concept related to subtyping is embedding. Eg the Integers are embedded in the Reals.

Another concept related to subtyping is when a class exposes one or more views as Patterns for structural typing (pattern matching) ('adt's, algebraic data types), and when some of the subnodes in this view are types. For example, the Rational class may expose the View of itself as "a / b", where a and b are Ints. This is also like a 'typeclass context' in Haskell, in that in general we have a Pattern like "a / b" with type variables in it (in this case 'a' and 'b'), and constraints on those type variables (in this case, that a is in the (typeclass) Int, and that b is in the (typeclass) Int). Recall that 'typeclass' in Haskell is just called a 'type' here, as all Oot types can have subtypes (but in a heterarchical structure, eg a type may be a subtype of multiple parent types) and all Oot types can be implemented in multiple ways.

Implementation dependencies are like dependencies in a package management system. Implementations can depend on types (all that is required is any implementation of the desired type), or 'concretely' on other implementations (we demand a specific implementation of a type, because we are going to break into its internals). For example, the Rational implementation can depend on the type Int (meaning that it makes use of Ints internally), or it could be eg a FFI binary containing optimized x86 code which calls subroutines from another binary package containing an implementation of Ints. Outside of FFI, a concrete implentation dependency is one which breaks encapsulation by accessing private variables in another implementation.

does Oot support concrete implementation dependencies aside from FFI at all? If so, does it force you to specify a specific version of the concrete dependency, to prevent the upstream author of the dependency from worrying about breaking code by changing Private variables? Perhaps it only supports concrete dependencies within the same module?

---

todo review haskell typeclass/java interface distinction again? it was something about existential types or something, somewhere on the haskell wiki perhaps.

---

AADTs: Algebraic Algebraic Data Types

eg saying that Rational is a type such that an expression involving the rational is equivalent to an expression of the form 'a / b' where a and b are Ints (and perhaps with the implicit mapping a <--> r.a , b <--> r.b, where .a and .b are fields of a rational instance r).

---

closed data types are in fact very useful; because if all you know is that you have a value of an open data type, you really don't know anything, because even for any property that all known instances of the type have in common, later you could discover another instance that has the negation of that property.

closed data types are eg useful for letting the compiler exhaustively check cases

(but if some cases have 'more data than expected' in them, the open data problem eg where you replace Cons(x,y) with Pair(Cons(x,y), some_metadata) but such that you can still match it against ordinary Cons(x,y) and bind x,y, ignoring the some_metadata, then that's fine, you still 'learned something' from the closed list of cases; the key is that the part that is 'open' is in some sense orthogonal to what you are learning by knowing the closed list of cases; in this example, the Pair(Cons(x,y), some_metadata) really is like a Cons of a list, so this datastructure really can be regarded as being the union of exactly its EmptyList? and Cons cases)

note that pattern matching on Haskell (ADT) datatypes achieves a kind of 'ad-hoc' polymorphism in a slightly different way from typeclasses; in a typeclass, the ad-hoc cases are defined in the instance (all together), but with pattern matching, the ad-hocness is defined at each use site (it has 'use site ad-hoc openness', i guess).

we want to have pattern matching, like Haskell, but we also want to 'open' a way to define new ways to pattern match on existing data types.

so, what we'll do is allow each View of a type to define its own ways to pattern match (its own set of cases (data constructors), etc). The (closed) set of cases available in a View is part of the interface signature of (one of the) interfaces supported by the View; eg its part of the typeclass signature, in Haskell terms.

in a way, this lets us support closed data types and open at the same time as follows; within a given View, we can have a closed list of cases (data constructor), but then we can switch to a different view and have a different list. That doesn't sound so different from Haskell's data types vs typeclasses; but what we're saying is that the SAME data value can masquerade as different data types in different places; so you can't eg create a parsing library whose signature demands linked-list-strings and rejects ByteStrings?, because the ByteStrings? can always be given a facade of a linked-list-string View.

---

so, note that each View can support more than one interface (typeclass).

---

the type system should allow the representation of units (feet, centimeters), types of units (length of space, duration), processing stages (unsanitized string from user input, sanitized string; uninitialized/initialized), program-specific message subtypes

---

in golang,

'arrays' are of constant length (the length is in the type) (like Python tuples) 'slices' are pointers to arrays. However, practically, slices operate as variable-sized arrays.

how to generalize this? is this just the typical way that parametric polymorphism (generics) works? i think it's a little different, eg we are not literally having a different method lookup table for every possible array length

--

vilhelm_s 2 days ago

But perhaps a better type system can still be helpful. E.g. F# supports units of measure, so you can declare 'dollar' as a unit, and write

    let calc_total (meal_cost : float<dollar>) (tax : float) (tip : float) =
       meal_cost * (1.0+tax) * (1.0+tip)

This way it is at least clear from the types that the numbers are meant to be multiplied, not added.

reply

S4M 2 days ago

I never used F#. In your example, would the code:

    meal_cost + tax

trigger a compiler exception?

reply

vilhelm_s 2 days ago

Yes, you get

    The type 'float' does not match the type 'float<dollar>'

There is an online typechecker, so one can try out F# without installing it: http://www.tryfsharp.org/Learn/scientific-computing#units-of...

reply

S4M 2 days ago

And how about:

    meal_cost * tax

?

This one makes sense in the real world, so I suppose an advanced type system allows the programmer to specify what operations are legit or not across different types.

reply

vilhelm_s 2 days ago

One could imagine systems for that, but units of measure doesn't do any customization of different operations. It's just unit checking for for arithmetic, like in high-school math.

reply

---

"Elm language limitations have become a real problem for me. The type system is F#-like: too limited to define Applicative, Monad, or any abstraction or data type that has a type parameter whose kind is not *. Also no higher-rank types or existential types. You can sometimes survive without these things, but eventually you reach a point where you need them. I’ve hit that point." -- https://pchiusano.github.io/2015-04-23/unison-update7.html

--

"A question to think about for type classes is, what is the best way to reuse variable names? Type classes, implicit arguments, and module functors all answer this question, but each comes with some unfortunate tradeoffs. My view here is that there is no need to rush. When our community collectively needs this kind of feature, we will be in a much better position to evaluate the trade-offs between these approaches for the problems we are facing in practice.

...

Until that time, I'd like to pursue the "scrap your type classes" approach which allows you to do explicit dictionary passing through some combination of higher-kinded polymorphism and rankN types. To me this is a minimal set of non-controversial features that get you a lot of what you want, so I think it makes sense to explore this route thoroughly before picking our poison with type classes, implicit args, or module functors. " -- https://groups.google.com/forum/#!msg/elm-discuss/oyrODCgYmQI/T2I_8L-AL6EJ

---

" Java’s type system simply isn’t very powerful or useful. Java actually contains two type systems, meshed together into an unsettling chimera. One of its type systems is bottom-up and vaguely algebraic, consisting of a few primitive types (integers of varying sizes, and single- and double-precision floating point numbers) and arrays of existing types. That’s it. It has int and double[] and char[][] but cannot represent anything more interesting (tuples, strings, variants, parameterized types). To represent those more structured types one has to use Java’s other type system, which is top-down– everything is a subtype of “Object”, and each variable stands not for the object itself, but to a reference to what might be an object of that type, or none (null).

The nastiness of this cannot be overstated. Java’s notorious NullPointerException?, a runtime failure associated with dereferencing a null pointer, is both a common and (from a debugging perspective) a usually-quite-useless error. Java’s type system lacks the power to verify that a String variable, at compile time, will actually hold a string, and not null, a value that must be handled specially by any method that takes a String (ditto, for any other object type) as input. The string type is not available; you must make do with what is, in fact, a (string option) ref— a mutable reference that may hold a String. " -- https://michaelochurch.wordpress.com/2010/10/29/the-next-secret-weapon-in-programming/

---

why Go doesnt use generics:

rsc 17 days ago

parent flag

I'm sorry, but no: Generics are a technical issue and are not a political one. The Go team is not against generics per se, only against doing things that are not well understood and/or don't work well with Go.

There are deep technical issues that must be solved to fit the idea of generics into Go in a way that works well with the rest of the system, and we don't have solutions to those. I wrote on my blog about one issue years ago (http://research.swtch.com/generic), but there are others too. Even supposing you get past the problem on that page, the next thing you would run into is how to allow programmers to omit type annotations in a useful, easy-to-explain way. As an example, C++ lets you write make_pair(1, "foo") instead of make_pair<int, string>(1, "foo"), but the logic behind inferring the annotations takes pages and pages of specification, which doesn't make for a particularly understandable programming model, nor something the compiler can easily explain when things go wrong. And then there's a princess in another castle after that one I am sure.

We have spoken to a few true experts in Java generics and each of them has said roughly the same thing: be very careful, it's not as easy as it looks, and you're stuck with all the mistakes you make. As a demonstration, skim through most of http://www.angelikalanger.com/GenericsFAQ/JavaGenericsFAQ.ht... and see how long before you start to think "was this really the best way to do this?" (For example, http://www.angelikalanger.com/GenericsFAQ/FAQSections/TypePa..., but note that the latter page is only one part of the FAQ, not the entire FAQ.)

To be very clear, we acknowledge this fact: there are definite disadvantages to not having generics. You either use interface{} and give up compile-time checking or you write code generators and complicate your build process. But there are also definite disadvantages to generics as implemented in existing languages, and there is a very large advantage to not compromising today: it makes adopting a better solution tomorrow that much easier.

As I said in the interview at http://www.pl-enthusiast.net/2015/03/25/interview-with-gos-r...:

> Go is more an engineering project than a pure research project. Like most engineering, it is fundamentally conservative, using ideas that are proven and well understood and will work well together. The research literature’s influence comes mainly through experience with its application in earlier languages. For example, the experience with CSP applied in a handful of earlier languages—Promela, Squeak, Newsqueak, Alef, Limbo, even Concurrent ML—was just as crucial as Hoare’s original paper to bringing that idea to practice in Go. Programming language researchers are sometimes disappointed that Go hasn’t picked up more of the recent ideas from the literature, but those ideas simply haven’t had time to pass through the filter of practical experience.

I believe generics is one of those ideas. It certainly needs at least one more iteration, possibly a few more than that.

---

types as just a bundle of assertions (this would unify eg graph structural types/graph patterns, and oop classes)

---

per-element type attributes:

does a value in a subset type (eg int) acquire all of the type attributes of a value of a superset type (ie reals)? There might be some attributes of the type 'real' that describe the type as a whole; for example, 'uncountable'. These should not be inherited by the subset type. By contrast, all attributes of the superset types which are 'per-element', that is, something that applies to each element of the type individually rather than some statement about the type as a whole, are inherited by the subset type.

---

" hermetic ...

what if we went to an alternate dimension, where python starts like a typed functional language, instead of a class-based oop one? ..

@template(y, z) def f_map(f: y >> z, s: [y]) -> [z]: out = [] for i in s: out = append(out, f(i)) return out

def nope(a: Integer) -> Integer: return a + 4

print(f_map(nope, [2, 4]))

def sum(n: Integer) -> Integer: sum of the numbers from 0 to n inclusively result = 0 for i in range(0, n + 1): result += i return result

print(sum(2000))

...

syntactic sugar : [Integer] for list types, y >> z for function types, Integer

"
Float for union types.

-- https://github.com/alehander42/hermetic

" dochtman 1 day ago

Those who like this might also like my language project, Runa:

A Python-like systems programming language. This means that the design borrows as much from Python as makes sense in the context of a statically-typed, compiled language, and tries to apply the Zen of Python to everything else. The most important design goals for Runa are developer ergonomics and performance. The compiler is written in Python and targets LLVM IR; there's no run-time. More information can be found on the project website.

https://github.com/djc/runa/

reply "

"

Animats 1 day ago

There have been other typed Python variants. RPython, in which PyPy? was written, is sort of one. Shed Skin tried to do it entirely via type inference, which is really hard across functions.

It's clear now that you want at least enough type inference in a language that LHS types of assignments and variable creations are inferred when possible. When you have that, as in Go, Rust, and even C++ to some extent, most of the declarations are in function definitions. There, you want them for documentation purposes anyway.

reply

keypusher 1 day ago

MyPy? is a pretty good typed Python variant. I believe the "optional type annotations" PEP used their style.

http://mypy-lang.org/

reply "

"

nly 1 day ago

> even C++ to some extent

C++ can also infer return types, the following is a valid C++14 function definition

    auto foo() {
        auto curry = [](auto x) {
            return [=](auto y) { return x + y; };
        };
        auto add42 = curry(42);
        return add42(58);
    }

which incidentally gets compiled to this:

    0000000000000000 <foo()>:
       0:	mov    $0x64,%eax
       5:	retq

reply "

" bkeroack 1 day ago

The value-add here is that it compiles to C and therefore the type enforcement is done at compile time. If you are OK with interpreted Python and runtime checking you can use https://github.com/prechelt/typecheck-decorator/

reply

alehander42 1 day ago

That looks cool! It's pretty different though, it's more like a "design by contract" tool. I have a similar one, more Python2 style dsl (it supports also function overloading through a kind of pattern matching) https://github.com/alehander42/py-matchete

reply "

---

already to oottoreads:

Self-Representation in Girard’s System U

Self-Representation in Girard’s System U, by Matt Brown and Jens Palsberg:

    In 1991, Pfenning and Lee studied whether System F could support a typed self-interpreter. They concluded that typed self-representation for System F “seems to be impossible”, but were able to represent System F in Fω. Further, they found that the representation of Fω requires kind polymorphism, which is outside Fω. In 2009, Rendel, Ostermann and Hofer conjectured that the representation of kind-polymorphic terms would require another, higher form of polymorphism. Is this a case of infinite regress?
    We show that it is not and present a typed self-representation for Girard’s System U, the first for a λ-calculus with decidable type checking. System U extends System Fω with kind polymorphic terms and types. We show that kind polymorphic types (i.e. types that depend on kinds) are sufficient to “tie the knot” – they enable representations of kind polymorphic terms without introducing another form of polymorphism. Our self-representation supports operations that iterate over a term, each of which can be applied to a representation of itself. We present three typed self-applicable operations: a self-interpreter that recovers a term from its representation, a predicate that tests the intensional structure of a term, and a typed continuation-passing-style (CPS) transformation – the first typed self-applicable CPS transformation. Our techniques could have applications from verifiably type-preserving metaprograms, to growable typed languages, to more efficient self-interpreters.

Typed self-representation has come up here on LtU? in the past. I believe the best self-interpreter available prior to this work was a variant of Barry Jay's SF-calculus, covered in the paper Typed Self-Interpretation by Pattern Matching (and more fully developed in Structural Types for the Factorisation Calculus). These covered statically typed self-interpreters without resorting to undecidable type:type rules.

However, being combinator calculi, they're not very similar to most of our programming languages, and so self-interpretation was still an active problem. Enter Girard's System U, which features a more familiar type system with only kind * and kind-polymorphic types. However, System U is not strongly normalizing and is inconsistent as a logic. Whether self-interpretation can be achieved in a strongly normalizing language with decidable type checking is still an open problem. By naasking at 2015-06-11 18:45

Functional Lambda Calculus Theory Type Theory 28 comments other blogs 5827 reads

---

http://stackoverflow.com/questions/4069840/lambda-for-type-expressions-in-haskell

---

" Curry-Howard only really becomes interesting once you have dependent types, and only becomes bullet-proof when your language is total. Haskell has neither property. The connection to C-H is something which might interest a large subset of Haskell programmers (who would likely take that interest into a study of Coq, Agda or Idris), but it has pretty much no bearing on the day-to-day usage of Haskell. "

vilhelm_s 2 days ago

I don't think the connection between Haskell and Curry-Howard is that strong (it's stronger since GADTs were added, but still, functions are not even terminating). Rather, I think the main thing that makes Haskell "mathematical" and easy to reason about is that it is pure, so you can reason about things equationally.

That will help verification no matter what framework you are using. For example, look at the seL4 verification. That was done in Isabelle/HOL, so it doesn't use Curry-Howard in any way. But even so, they proceeded by writing two versions of the operating system, one in C, and one in Haskell to make it easier to reason about.

reply

---

"...the philosophy that verification should be based on explicit types in the original program source. This intricately ties the process of authoring software with that of verifying it. The result is needlessly constraining both the developer and the verifier. It only lets you (easily) write code within what it can prove, and only lets you prove properties that can be expressed by the types that you use.

Other approaches say, we'll let people write code however they feel most comfortable doing (more or less), using types whose expressivity is defined not by the limits of the verifier but only by various concerns over language complexity, mental overhead, performance and teamwork, while we let the verifier prove whatever types it can. If it proves that the variable x is of type "an integer which is always equal to the current time in seconds modulo seven, except on Saturdays when it's always zero", then that's great! " -- https://news.ycombinator.com/item?id=10139235

pron 1 day ago

P.S.

I do, however, believe in the combination of familiar "cognitive" languages alongside verification tools. For example, see how Amazon uses TLA+ to verify their Java programs[1]. This alone is more real-world usage than Haskell has ever seen.

[1]: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext

reply

pron 2 days ago

... I have two issues with your argument. The first is the (implied, I think) assumption that C-H is the only way to apply math to programming languages. I think C-H has so far disappointed, because 1., people don't seem to want it, and 2. because other verification systems (like KeY?) or the verifiable imperative, reactive real-time languages of the eighties (like Esterel) whose descendants are still in use today, have so far been used to much better effect. ...

http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext

---

"Nevertheless, there is a core theory of operations that can readily be adapted to a number of local purposes by suitable expansions in each cas e. This has the following featu res: (i) Operations are in general allowed to be partial. For example, the operations of division in algebra and integration and differentiation in analysis are not everywhere de fined. (ii) Operations may be applied to operations. For example, one has the operation of composition of two operations, the operation of n - times iteration of a given operation, the “do...until...” operation of indefinite iteration, etc. (iii) In consequence of (ii) , a generally adaptable theory of operations is type - free. (iv) Extensionality is not assumed for operations. For example, the theory should allow the indices of partial recursive functions to appear as one model. (v) The language of the theory is at least as exp ressive as the untyped lambda - calculus and the untyped combinatory calculus. (vi) Though logical operations of various kinds on p ropositi ons and predicates may appear in particular applications, first - order classical or intuitionistic predicate logic is taken a s given.

These features form the general operational perspective "

http://math.stanford.edu/~feferman/papers/Op_Persp_3Routes.pdf

---

feferman's System W:

https://queuea9.wordpress.com/2010/03/19/fefermans-theory-w/

https://queuea9.wordpress.com/2010/01/17/how-strong-a-type-theory-do-we-need/

" Feferman presents a theory W, in the spirit of Weyl’s work, in which Weyl’s program (of reconstructing the mathematics of the reals on predicative foundations) can be carried out. This theory W is essentially a theory of general recursive functions, described by individual terms, and classified by what a Computer Scientist would see as simple types (base type N for natural numbers, function types S\stackrel{\sim}{\rightarrow} T for partial functions from S to T, and cartesian production types). Classification is done with an explicit membership predicate \in, and the simple types are expressed as class terms of the language. (So types are not a distinct syntactic category; rather, they are expressed as terms of the language, and the connection with individual terms is given by an atomic formula of the language, using the \in predicate.)

Theory W is based on Beeson’s Logic of Partial Terms (LPT), which has an explicit predicate \downarrow for definedness. In W, \downarrow is used for termination of general recursive functions. There are axioms for definition by primitive recursion and search, as well as induction, in the form that if a\in\mathcal{P}(N), and 0\in a and a is closed under successor, then every n\in N is in a. Here, \mathcal{P}(N) is defined as N \stackrel{\sim}{\rightarrow} \{ 0, 1 \} (that is, as the class of characteristic functions for subsets of N). This theory does not allow us to state that a class T_1 is a member of another class T_2, unless of course the former is representable by an individual term.

Despite its expressivity, W is a conservative extension of Peano Arithmetic. " -- https://queuea9.wordpress.com/2010/03/19/fefermans-theory-w/

(the following is much easier to read on PDF page 8 of http://math.stanford.edu/~feferman/papers/psa1992.pdf) " As indicated in Section 2 above, in order to represent the notions of modern analysis directly and develop analysis flexibly it is necessary to have not only the set R of real numbers but also for any set S , its definable subsets XxSx? ={ ∈ :()} φ , and for any sets X and Y also the sets X × Y and X – >> Y , where the latter is understood to be the set of all partial functions from X to Y . Now if functions were defined as many-one relations as in set theory, X – >> Y would simply be the set of all many-one ZXY ⊆× , and this would call on P( X × Y ) for its definition; that route would, in effect, take us back to Zermelo's set theory. The crucial first step toward a flexible, predicatively justifiable system is to treat functions and classes as conceptually independent basic notions, i.e. with neither explained in terms of the other. A system taking this lead was worked out successively in (Feferman 1975, 1985, and 1988). We follow the last of these papers in describing the system W (so designated in honor of Weyl) presented there in detail.

The language of W is two-sorted, with individual variables a, b, c, ..., x, y, z ranging over a universe containing numbers, sets, functions, functionals, etc., and closed under pairing, while the variables A, B, C, ...X, Y, Z range over classes or (variable) types . Note the terminological shift here: sets will be reserved for subclasses of a given class S which have a characteristic function. There are constants for specific individuals and functions (indicated below); there are also binary operations 〈〉 xy xy ,() and , where the latter is interpreted as the value of x at y when x is a partial function and y is in its domain, otherwise undefined. Individual terms s,t,... are built up from individual variables by use of the given constants and operations by closure under the general process of explicit definition, including function definition ().(). λ xStx ∈ Class terms S, T,... are built up from class variables and the class constant N by closure under the operations: S × T, S – >> T and {

xS ∈ φ ( x )} where φ is a bounded predicative formula (explained below). Formulas of W in general are built up from atomic formulas stt tS =↓ ∈ , and by the propositional operations and quantification with respect to both individual and class variables; t ↓ is used to express that t is defined. The bounded predicative formulas admit no quantification over class variables, and individual quantifiers are restricted as: () (). ∀∈ ∃∈ xS xS φφ and By definition, ( ) { ST z →=∈ ( S – >> T )( ) }. ∀∈ ↓ xSzx

The individual and function constants are 0 and Sc (for successor on N ), and μ (for the non-constructive least number or search operator) , P 1 and P 2 (for projections of pairing), D (for definition by cases), and Rc N (for definition by recursion on N) . The function axioms of W follow these intended meanings together with usual axioms for explicit definition.

Taking 10 01 ==→ Sc( ), ( ) ( { , }) we write P SS for the class of subsets of S regarded as the class of characteristic functions on S . Then for aS ∈ P () we write xa ax ∈= for ( ) 0 . In particular, the axiom for μ is simply

() ) [( )( ) () ] μμ μ ∈→∧∀∈ ∃∈⇒∈ P(P NN N) annaa

...

Induction on N is taken as so-called set induction : (Ind Set ()[0 (n )(()))] . Sc ∀∈ ∈∧∀ ∈⇒ ∈ ⇒∀∈ ∈ aannanana P NN

Using the μ operator one shows in W that sets are closed under numerical quantification, since ∃∈⇔ ∈⇔ = nna aaaa ()() (()). μμ 0 It follows that every arithmetical formula defines a subset of N ; then by Ind Set , we obtain the induction scheme for arithmetical formulas. The logic of W is assumed to be that of classical two- sorted predicate calculus. Hence the system PA of classical first-order arithmetic is contained in W.

The main meta-theoretical result about W is the following: Main Theorem W is proof-theoretically reducible to PA and is a conservative extension of PA.

" -- Why a little bit goes a long way: Logical foundations of scientifically applicable mathematics by Solomon Feferman, section 5, page 8


"

2. Generics aren't exactly optional in Rust. Let's assume for the sake of argument that generics are a bad feature that languages should not have (something I completely disagree with, but in any case). Even supposing this were true, it's not like Rust would be a better language without them. Rather, the language could not exist, because it would be impossible to satisfy its core goal of zero-overhead, runtimeless memory safety. You couldn't have smart pointers without generics; you couldn't have iterators; you couldn't have Option; you couldn't have any functions that take and return pointers at all because lifetimes are a form of generics. Go is able to get away with not having generics because it leans heavily on having a runtime to support the built-in data structures and on garbage collection to make memory management decisions at runtime. Not so with Rust, which is designed to bake all that information into the compiler to avoid the overhead of a runtime and of garbage collection. " -- https://news.ycombinator.com/item?id=10208488 (pcwalton)


in R, "...when you attempt to combine different types they will be coerced to the most flexible type. Types from least to most flexible are: logical, integer, double, and character. "

---

---

if you imagine taking something like the Lua 5.1 VM and building a BASIC-like language out of it, one thing you come to is:

ok, well we have a <= operator, but we want a way to use it with custom types (adhoc polymorphism)

with our 'additive interfaces/mixins/type attributes' model it may not always be clear how a given function (such as <=) is implemented for a given tuple of objects, because the function may inherit multiple implementations from its various 'type attributes' -- unless this is forbidden by our conception of mixins (eg one object cant have two mixins that would implement a function in a different way, unless when adding them the user explicitly specifies which one takes precedence for each shared operation); or unless there is a multiple inheritance 'precedence' system such as eg Python's to resolve conflict; or unless we go back to giving things a single 'type' (in which case we still have to adopt one of the other solutions in addition, i guess).

---

we may want to allow a 'multiple dispatch' system, in which we can define multi-input functions separately from the class definitions of all of their targets and have arbitrary combinations of target types, with a traditional 'single dispatch' oop-ish system, in which case dispatch is based only on the type of the object 'containing' the method, as follows:

single dispatch is required when we access the encapsulated 'internal state' of objects. Multiple dispatch is allowed otherwise.

---

should we restrict things that access encapsulated 'internal state' of objs to be single-inheritance, principal types rather than 'type attributes'/mixins/multiple inheritance? NO. The restriction is to single DISPATCH, not single INHERITANCE. However, to keep things clear, which internal state variables they access is part of their signature.

---

mb oot's type inference could be bidirectional (using unification) within a module (or within a function?) but unidirectional between modules.. or maybe no type inference between modules, bidirectional within a function, unidirectional between functions

---

re: Hoon

" "Odor" is a class of types that doesn't seem to have any existing term. It's a nominative type system for atoms, as opposed to the rest of our type system, which is purely structural. "

---

Oz types are interesting: https://mozart.github.io/mozart-v1/doc-1.4.0/tutorial/node3.html

" Most of the types seem familiar to experienced programmers, except probably Chunk, Cell, Space, FDInt and Name. We will discuss all of these types in due course. For the impatient reader here are some hints. The Chunk data type allows users to introduce new abstract data types. Cell introduces the primitive notion of state-container and state modification. Space will be needed for advanced problem solving using search techniques. FDInt is the type of finite domain that is used frequently in constraint programming, and constraint satisfaction. Name introduces anonymous unique unforgeable tokens. "

---

Structural typing / duck typing in interfaces

" jerf 4 hours ago

"Take interfaces. In Java you might start with them. In Go - in the best case - they emerge, when it's time for them."

And it's a relatively subtle language feature that does this, the way that any struct that implements a given interface automatically conforms to that interface without having to be declared. Which means you can declare an interface that foreign packages already conform to, and then freely use them. Which means that you can code freely with concrete structs to start with, and then trivially drop in interfaces to your code later, without having to go modify any other packages, which you may not even own.

I completely agree that on paper Java and Go look virtually identical. But the compounding effect of all those little differences makes them substantially different to work with. Good Go code does not look like good Java code. You'd never confuse them.

reply

kasey_junk 3 hours ago

There is a big downside to structural typing as golang implements it though. Refactoring tools. They quite simply cannot do the same kinds of safe refactoring something like a Java refactoring tool can do, because you can't be sure if the function you are trying to rename, add parameter too, etc. is actually the same function in question.

There are times when I love the structural typing aspects of golang (trivial dependency inversion) and there are times when I hate it (nontrivial renames), its one of many trade-offs you have to be prepared for in golang.

reply " [1]

" pcwalton 3 hours ago

> Which means you can declare an interface that foreign packages already conform to, and then freely use them.

But you cannot do the reverse: you cannot make a type from a foreign package conform to your interface by adding new methods to it. This is because, with structural typing, it's not safe to add methods to types in other packages, since if packages B and C both were to add a conflicting method Foo to a type from package A, B and C could not be linked together. This is a major downside of structural typing for interfaces. Swift, for example, has the "extension" feature, and Java's design allows for it in principle, but it's fundamentally incompatible with Go's design.

reply " [2]

"

justinsaccount 3 hours ago

> But you cannot do the reverse: you cannot make a type from a foreign package conform to your interface by adding new methods to it.

I thought you could.

You don't add the methods directly to it, but you can easily embed the foreign type into a new type that confirms to the interface you want.

  type FooWrapper struct {
    Foo
  }
  func (fw FooWrapper) SomeFunc() {
  ...
  }

reply

pcwalton 2 hours ago

That's making a new type, which causes a lot of friction. For example, a []Foo array is not castable to a []FooWrapper? array without recreating the entire thing.

reply "

[3]

---