Bayle Shanks's website: proj-oot-old-150618-ootTypeNotes2

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

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

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

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

...

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

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:

eliminate both disjunction and negations: this jibes with the result of my ill-fated psych pilot experiment on human category learning (the result was that people not trained in CS are mostly only good at conjunctive categories)
eliminate disjunction: one problem with this is, how do you represent ad-hoc polymorphism? E.g. something has the type/typeclass-membership/attribute Number if it is an Int or a Float or a Rational or (whatever else a Number typeclass instance has been defined for), etc. One could say that this is 'not really a type' and so we don't have to worry about it, but practically for the purpose of type inference tractability it seems like the same thing to me, although i haven't thought too hard about that so hopefully i'm wrong
eliminate negations (monotonic logic): this would seem to rule out types like 'pure functions', which may be important for Haskell-ish annotation of side effects, but one could define these at a lower level (e.g. 'a function is impure if it is marked impure or if it is composed of something impure and is not marked pure') and do a separate type inference step at that level, and then at the (main) type inference level everything is monotonic

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:

no generic functions in protocols (but see: https://news.ycombinator.com/item?id=7896161 ) (see also http://schani.wordpress.com/2014/06/11/associated-types-considered-weird/ and https://groups.google.com/forum/#!topic/swift-language/3PtydRXR0ao and http://www.artima.com/forums/flat.jsp?forum=106&thread=270195 )
generic enums theoretically exist but 'not yet implmented' in compiler
assignment of an empty list constant as a default value to a generic parameter caused a segfault in the compile

---

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.

...

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] 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 }

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?