proj-oot-ootTypeNotes5

"2. Generics (both types and immutable constraints), I think C++1z has the right approach to this (and constexpr and constant arrays are nice and are able to provide more hints to the compiler)."

---

think about the code examples in these subsections:

http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#generics

http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#aside-generic-inference-and-the-turbofish ---

also, in http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#generics , i don't quite understand why need need two <T>s in the following declaration:

// Implementing functionality for all choices of T.
// Note that the "impl" is also Generic here.
// Hopefully this in conjunction with the previous
// example demonstrates why the extra <T> is necessary.
impl<T> Generic<T> {
    fn new(data: T) -> Generic<T> {
        Generic { data: data }
    }

    fn get(&self) -> &T {
        &self.data
    }
}

My guess based on other examples with <> after 'impl' later on that same webpage is that the first <T>, impl<T>, is just saying that the following declaration will have a type variable in it ('T'). Which i don't see why we really need, because we can infer it from the presence of capital T inside Generic<T>, right? But i guess this is like how we want to have 'lambda x: x + 2' not just 'x + 2' and let the compiler find out that 'x' hasn't been previously defined; also, in some examples further down that webpage, there is stuff like:

impl<T: Clone> Clone for Generic<T> { fn clone(&self) -> Self { Generic { data: self.data.clone() } } }

where there is a 'trait bound' on 'T' (why don't they call it a 'type bound'?) that says that T must implement trait 'Clone'.

i wonder if this stuff could be simplified by using ordinary function notation here, something like:

Clone for Generic<T> := fn(T :: Clone) {...}

(obviously this isn't quite right, but you see where i'm going; you are explicitly representing that T is a parameter using ordinary function notation)

---

if we have 'type attribute', need a syntax to say, within a type annotation "x has type attribute A, AND x also has type attribute B". Eg if you want to say that type "T" implements interface 'Box', and also "T" implements interface 'Clone', would you say:

T <: Box && T <: Clone

?

also, should we reserve '<:' for subtypes and have some other syntax for 'implements'?

also, interestingly, these are logical assertions, not imperative computations.

is this sort of notation what you'd find in the arguments of a function-style syntax for type bounds in genericity, as in the previous section? eg

... := fn(T :: T <: Box && T <: Clone)

that doesn't look quite right, because you expect to see stuff like

x :: int16

meaning "x ISA instance of type int16", but "T :: T <: Box && T <: Clone" up there means "T SUCH-THAT T is a subtype of Box and T is a subtype of Clone"

why not just have

T :: Box && Clone

to mean '(T s.t. T IS Box) AND (T s.t. T IS Clone)' where IS combines ISA and isSubtype as noted previously? That seems a little ambiguous, though.

hmm.

---

in Haskell, one reason for the "monomorphism restriction", according to [1], is to prevent surprising repetition of computation; eg without the monomorphism restriction, in

   genericLength :: Num a => [b] -> a 
   let { len = genericLength xs } in (len, len) 

each 'len' in '(len, len)' will be computed separately, so 'genericLength xs' will be evaluated twice. In [2], CaleGibbard? explains "The trouble is that typeclasses essentially introduce additional function parameters -- specifically, the dictionary of code implementing the instances in question. In the case of typeclass polymorphic pattern bindings, you end up turning something that looked like a pattern binding -- a constant that would only ever be evaluated once, into what is really a function binding, something which will not be memoised.".

So i guess CaleGibbard? is saying that in this case

   let { len = genericLength xs } in (len, len) 

is really sorta like

   let { len = genericLength xs } in (len(type(x)), len(type(x))) 

where type(x) is the type of the elements in the list xs. The idea seems to be that if you actually had

   (f(y), f(y))

then no one would be surprised that f(y) is being evaluated twice, but when you have

   (len, len) 

it's surprising.

But imo the surprise here is only partially due to that, it also comes from the semantics of 'let'. If you have

let { len = f(x) } in (len, len)

and f(x) gets called twice, that's a little surprising, because it look like 'len = f(x)' is an imperative variable assignment which will be evaluated before the following expression; but actually it's more like a lightweight macro that is substituted into the following expression before it is evaluated.

---

if we want to allow heterogenous lists, we could just have an 'any' type and do:

list<any>

---

if we want to use function syntax for higher-order types/type constructors like 'list' (note: Haskell's special syntax for the list type constructor, [x], is great), i guess that would look like:

tlist int

where 'tlist' is the type constructor for list, following a convention of prepending 't' for 'type' to types (so actually it would be:

tlist tint

) (that 't prepend' convention is ugly)

this looks a lot like how Haskell does it. It does seem more confusing than list<int> though.

---

this example shows the need for interfaces that can refer to their own type in the signatures of their functions:

" Consider a modified version of Iterator -- StateMachine?.

trait StateMachine? { type NextState?: StateMachine?; fn step(self) -> Option<Self::NextState>;; }

Ok, so a StateMachine? is some type that you can tell do a step, and it will turn itself into a new StateMachine? of some kind. Let's try to write that out as a generic trait:

trait StateMachine?<NextStep?: StateMachine?<UHHH_WHAT_GOES_HERE>> { fn step(self) -> Option<NextState?>; }

Trying to express StateMachine? as a generic trait leads to infinite type recursion! Because generics are inputs, all of the types need to be provided by the consumer of the interface. Which, in this case, is the interface itself. That said, there is a way to resolve this without associated types: virtualization!

trait StateMachine? { Box is magic! self can be type Box<Self>. This doesn't work with e.g. Rc<Self>, because *magic*. fn step(self: Box<Self>) -> Option<Box<StateMachine?>>; }

This expresses much the same intent as the associated type code. We consume ourselves, and we yield something that implements the interface. However, in order to get this working we have to mandate that all StateMachines? must be boxed up, and after the first call to step, the type of the resultant StateMachine? will be completely unknown. With associated types, nothing needs to be boxed, and concrete code always knows the type of a StateMachine?. "

-- http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#associated-types-1

---

fn min<I: Iterator<Item = T>, T: Ord>(mut iter: I) -> Option<I::Item> {...}

equivalent to

fn min(mut iter: I) -> Option<I::Item> where I: Iterator, I::Item: Ord,

-- http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#associated-types-1

---

there's gotta be a simpler/more uniform way:

http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#associated-types-1

this seems to be saying that the rules are different from template arguments vs. explicit type variables?

perhaps Scala's got it? Just treat template arguments and type variables as the same?

---

i think we can reduce complexity vs. Rust by only supporting the 'virtualization' method and not the 'monomorphic' method described in http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle for generics

---

i think we can reduce complexity vs. Rust by allowing direct logic-style assertions of equations between types, rather than having syntax for special cases of this (see http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle#associated-types-1 and http://cglab.ca/~abeinges/blah/rust-reuse-and-recycle/#where-clauses )

---

 tptacek 1 hour ago

Sometimes. Other times, generics are a tool that development teams use to amplify complexity.

reply

lmm 1 hour ago

Giving your team more powerful tools should always be a positive. If you don't trust them not to do harmful things with them then you have bigger problems.

reply

tptacek 1 hour ago

It doesn't feel like that's a strategy that worked especially well for Scala or C++. Go isn't the only language that removes powerful tools: all the strict functional languages do too!

reply

pcwalton 1 hour ago

The issues that Scala and C++ have are far beyond just "having generics". Classical (ML-style) generics are an incredibly simple feature, much more so than, say, built-in channels.

reply

tptacek 56 minutes ago

I agree and I like generics, but I think it's hard to argue that generics have never made a complicated project more complicated.

reply

pcwalton 51 minutes ago

I'd say typeclasses, templates, and variance have, sure. Those are separate features from generics in my mind. (But you could reasonably lump them all together under the heading of "generics" and I won't argue too much.) :)

reply

---

good example of the downsides of something like Golang, where you do have interfaces but you don't have parametric polymorphism:

jamesaguilar 777 days ago

One nice thing these examples also do is make it really simple for detractors to point out what they don't like about it. My #1 gripe about go, for example, is this: https://gobyexample.com/sorting-by-functions

package main; import "sort"; import "fmt"

type ByLength? []string;

func (s ByLength?) Len() int { return len(s) } func (s ByLength?) Swap(i, j int) { s[i], s[j] = s[j], s[i] } func (s ByLength?) Less(i, j int) bool { return len(s[i]) < len(s[j]) }

func main() { fruits := []string{"peach", "banana", "kiwi"} sort.Sort(ByLength?(fruits)) fmt.Println(fruits) }

In a few other languages:

    // C++
    sort(vs.begin(), vs.end(), 
         [](const string& l, const string& r) -> bool { 
             return l.size() < r.size();
         });
  1. Python vs.sort(key=lambda s: len(s))

When they fix this, Go might be the perfect language for me. Until then, I'm not touching it with a pole.

---

 jnbiche 2 days ago

This looks like a very well-written, easy introduction to making simple, dynamic programming languages (not surprising given the author's writing background).

But everyone writes about how to build these kinds of basic Forths, or Lisps, or reverse polish notation calculators. To be honest, once you've learned the basic technique, writing a toy dynamic language interpreter is pretty easy. Even adding a toy JIT isn't very hard, and there are multiple guides online on how to do this using Luajit, or Libjit, PyPy?, or LLVM, etc.

What I want more than anything is a guide written on the same level on how to build a toy statically-typed language, with algebraic data types. And even better, some basic discussion on how to learn about implementing advanced techniques like refinement, or linear, or dependent types (I realize these are extremely complex topics).

Every discussion I find on these topics is in dense academic papers. I'm slowly making headway, but it's a slog.

The only good resource I've found so far (and it's an excellent one) is Andrej Bauer's Programming Languages Zoo. But as far as I know, it's all (very helpful and instructive) source code, with no accompanying tutorials.

Is there no very simple introduction on writing a simple ML, with type checking? Any recommended resources?

It's possible that Butterick intends to cover these topics in later chapters, in which case I can't wait to read the book.

reply

orlandohill 2 days ago

These should get you started. The last two are by Simon Peyton Jones, one of the creators of Haskell.

One Hour ML https://vimeo.com/64593770

Algorithm W Step by Step http://catamorph.de/documents/AlgorithmW.pdf

Implementing functional languages http://research.microsoft.com/en-us/um/people/simonpj/Papers... http://research.microsoft.com/en-us/um/people/simonpj/Papers/pj-lester-book/

The Implementation of Functional Programming Languages http://research.microsoft.com/en-us/um/people/simonpj/Papers... http://research.microsoft.com/en-us/um/people/simonpj/Papers/slpj-book-1987/index.htm

reply

jnbiche 2 days ago

Oh, those are great, thanks. Not big on videos, but the Algo W pdf is great, and the last book is exactly what I need, and looks to answer some of the questions I'm running into doing this on my own (3rd one looks a little advanced for me at this point, maybe after I get through the Peyton Jones textbook).

reply

nteon 2 days ago

Pierce's Types and Programming Languages ( https://www.cis.upenn.edu/~bcpierce/tapl/ ) is great - I'm working throught it now. Its goes through both untyped and statically typed languages. It also goes into how to implement these things in OCaml.

reply

jnbiche 2 days ago

Yeah, I think I'm going to have a break down and shell out the dough for Types and Programming Languages. It's exactly what I need now.

reply

cgag 2 days ago

I belive this is trying to fill that niche: http://dev.stephendiehl.com/fun/

reply

samth 2 days ago

There is a simple ML-like language implemented in Racket, called plai-typed, which is used by some people for teaching the PLAI programming language book. You can see the implementation here: https://github.com/mflatt/plai-typed

reply

heimp 2 days ago

It looks like Pyret was first written in Racket. I think it's optionally typed, though.

https://github.com/brownplt/pyret-lang-resugarer

reply

mkolosick 2 days ago

As the sibling comment mentions, Pyret was originally written in Racket. It's now self-hosted, and I'm working on rewriting the typechecker so if you want I can answer questions about that. The current development is all done on https://github.com/brownplt/pyret-lang

reply

sklogic 2 days ago

Not in Racket, but still a Lisp: https://github.com/combinatorylogic/mbase/tree/master/src/l/... https://github.com/combinatorylogic/mbase/tree/master/src/l/lib/ml

reply

jnbiche 1 day ago

That is quite a broad and instructive project, very interested to see the Prolog type checking you describe below in action. Thanks!

reply

jnbiche 1 day ago

That is quite a broad and instructive project, very interested to see the Prolog type checking you describe below in action. Thanks!

reply

ics 2 days ago

Not the tutorial form you probably want but I've had this bookmarked, it may be interesting:

http://www.cse.chalmers.se/edu/year/2015/course/DAT150/ http://www.cse.chalmers.se/edu/year/2015/course/DAT150/lectu...

reply

sklogic 2 days ago

> What I want more than anything is a guide written on the same level on how to build a toy statically-typed language, with algebraic data types.

The answers here might be useful: http://stackoverflow.com/questions/12532552/what-part-of-mil...

> Is there no very simple introduction on writing a simple ML, with type checking? Any recommended resources?

I'd recommend reading A. Field, P. Harrison, "Functional Programming". Despite the title, the book is about implementation techniques.

P.S. I keep suggesting to everyone interested in implementing type systems to use a very simple technique: find an embeddable Prolog compiler for your language of choice (e.g., MiniKanren? for Racket), and then simply emit a flat list of Prolog equations out of your source language AST (do the lexical scoping pass first). Easy. And easily extendable to dependent typing and all that fancy stuff.

reply

nickpsecurity 2 days ago

"find an embeddable Prolog compiler for your language of choice (e.g., MiniKanren? for Racket), and then simply emit a flat list of Prolog equations out of your source language AST (do the lexical scoping pass first). Easy. And easily extendable to dependent typing and all that fancy stuff."

So, you represent the AST associations and type-checks as Prolog logic rules that operate on predicates describing the AST? And the inference engine runs through it to dump out true or false for various predicates and rules? Am I understanding it right?

Also, didn't realize Prolog could handle dependent types and such. That's neat to know.

reply

sklogic 1 day ago

For example, you have an AST node for 'x + 2', encoded as 'apply(apply(var("+"), var("x")), const("2"))' (we're talking about ML, so it is curried here).

Firstly, all the expression nodes must be annotated with type tags: 'A1:apply(A2:apply(A3:var("plus"),A4:var("x")), A5:const("2"))'.

Then your typing pass walking over this segment of AST would generate the following (mostly trivial) equations

    A5=integer  // from constant type
    A4=Vx
    A3=Vplus
    A3=fun(integer, fun(integer, integer)) // from environment lookup
    A3=fun(V1, A2) // application rule
    A2=fun(V2, A1) // application rule

Then this long Prolog query (all equations are comma separated) is executed and you'll get all An type values to attach to your AST, as well as variable x type.

> Prolog could handle dependent types

It's Turing-complete. You can encode anything you want in it.

reply

---

already copied this to plBook:

tel 777 days ago

I think the biggest advantage of parametric polymorphism comes from program analysis, not just increased capability. The notion of parametricity depends crucially on parametric polymorphism and is super useful. Parametricity is the property that says greater polymorphism means lesser variation in implementation. Highly parametric functions can be almost completely described by their types along meaning it provides incredibly high value as documentation.

The most common simple example is reasoning about the following pair of functions

    f :: a -> a           g :: Int -> Int

While (f > g) obviously, we can completely characterize the behavior of `f` while we know almost nothing at all about `g`. Up to non-termination, `f` must be `id` while `g` can be any recursive function on integers.

                g a = 3
    f a = a     g a = a * 2
                g a = if (a == 0) then 1 else a * g (a - 1)

If you hold in advance the triviality of this example, then we can already notice how much better documentation `f`'s type provides than `g`'s. We also can produce a list of properties and laws about `f`'s behavior that we cannot easily do with `g`. This means that I'm able to reason about `f` better and more confidently.

---

So we can take it up a notch. Consider Functors in Haskell. In order to avoid the full generality, let's just say Functor is the container interface and types like [], Set, and Map instantiate it. This gives them the function

    fmap :: (a -> b) -> f a -> f b

where `f` is specialized to the particular container of interest

    fmap :: (a -> b) -> [a]     -> [b]    
    fmap :: (a -> b) -> Set a   -> Set b  
    fmap :: (a -> b) -> Map k a -> Map k b      -- for some key type k

Now what can we reason about `fmap`s knowing only their type? Well, since the type `a` contained inside each container is unknown (or, to be more clear, any implementation of fmap must work for any type `a` and thus it's "unknown" in that we can't take advantage of information about it) then the only thing `fmap` is capable of doing is applying the first function to those types.

Furthermore, since every mention of `a` vanishes in the result of the function we know that each value in the input container must either be transformed by the input function or dropped.

    -- a specific example, not a general function
    fmap f [a, b, c] = [f a, f b, f b]

In this way, parametricity has pruned down the possibilities of functions that can implement `fmap` a great deal. If `a` or `b` were specialized to specific types then this would not be the case as we'd have a large variety of specific functions that could apply to each one of them.

    notFmap :: (Int -> Char) -> [Int] -> [Char]
    notFmap f [n1, n2, n3] = [f (n1 + 2), head (show n2), chr n3] ++ "hello world!"

Indeed, in order to ensure that type-checking `fmap`s behave correctly we say they must follow a few laws. First, they respect function composition and second they respect identity

    fmap g (fmap f x) == fmap (g . f) x
    fmap id x         == id x

And we only ever need to check the first one because the second one is already guaranteed by a more sophisticated parametricity argument.

    fmap f []     = []
    fmap f (x:xs) = f x : fmap f xs

---

The take away is that while you can definitely write something that "maps over containers" without using parametric polymorphism, you have a harder time taking advantage of parametricity to have the types provide guarantees about the safe behavior of functions. Types (and in particular type inference) can sometimes make things more expressive, but their primary power lies in making things easier to understand and reason about.


shachaf 775 days ago

The last part is backwards -- when F is a functor, the only law we need to check is the identity law, but checking the composition law isn't enough. For example,

  fmap _ _ = []

satisfies fmap f . fmap g = fmap (f . g), but not fmap id = id.


tel 775 days ago

Whoops, that's correct.


andolanra 777 days ago

I'm going to note that even if Go added some kind of parametric polymorphism at this point, it still wouldn't have the same advantages as parametric polymorphism in Haskell and related languages. In Go, you can branch on types at runtime, so in a hypothetical generic Go, you could write something which appears to only ever return its argument, but does something special if the argument is of a particular type:

    func<T> id(t T) T {
      switch t := T.(type) {
        case int: return t + 1;
        default:  return t;
      }
    }

The ability to examine on types at runtime can enable some interesting programs, but it also means that you don't get guarantees like you do in languages like Haskell. An example of this biting someone in practice is this blog post[1], where the author reasoned that because a library function expected an io.Reader, all it would do is use the Read method as exposed by Reader. In reality, though, the function was able to branch on the type and determine whether it also exposed a Close method, and called that if it could. That kind of feature destroys the useful static guarantees provided by parametric polymorphism in other languages like ML or Haskell.

[1]: http://how-bazaar.blogspot.co.nz/2013/07/stunned-by-go.html


tel 777 days ago

As a second addendum, while andolanra's comment is completely true, you can actually do type dispatch in Haskell using the Typeable machinery; however, the type system requires that you mark your types when this occurs.

    what :: Typeable a => a -> a

Here `what` is no longer guaranteed to be `id`. Instead, we can translate it like this

    what :: (a -> TypeRep) -> a -> a

where `TypeRep?` is, as it sounds, a representation of the type of a returned dynamically. This means that we can do careful coercions to, say, be `id` unless `a` is `Int` in which case we add `1`.

Suffice to say that the degree of guarantee breaking that this kind of code invites makes Typeable a very specialized library that's almost never recommended without a "unless you really know what you're doing" kind of warning.


" > TypeScript? has has union types i.e. "number

string" which are similar to algebraic data types.

I understand that you said "similar", but there's actually a big difference that should be mentioned explicitly, namely that algebraic data type (ADT) sums always have "constructors" which you can use to disambiguate with. That means that you can meaningfully do the equivalent of "int

int" whereas for union types that would just be "int". (I'm sure you already know this, I'm just pointing this out for those who may not know or appreciate the subtleties.) Example:
    data Maybe a = Nothing | Just a

In this example the "constructors" are Nothing and Just.

... " -- [3]

 spicyj 19 hours ago

Flow has pretty good support for tagged unions like this which act like ADTs:

http://flowtype.org/blog/2015/07/03/Disjoint-Unions.html

reply

fleshweasel 19 hours ago

This is great. Seems less cumbersome than TypeScript?'s user defined type guards for distinguishing cases of a union. The sentinel value concept is something you could at least steal when creating user defined type guards to make them simpler, at least.

reply

wereHamster 21 minutes ago

TypeScript? union types and Flow tagged unions are nice to have, but to make them really useful you also have to provide a good way to pattern match on them. And there they both are still way behind Haskell.

reply

lomnakkus 19 hours ago

That's interesting! I haven't paid much attention to Flow since trying out the initial release and finding it a bit lacking. (But then, I'm used to GHC/Haskell, so everything lacking!)

I truly feel that "disjoint unions" is one of those things you don't appreciate the true value of until you've used them for quite a while. The real eye-opener for me was implementing a state machine and finding that I could explicitly state exactly which bits of the state machine would propagate to $NEXT_STATE at every step... and have the compiler double-check for me that I got it right.

fleshweasel 19 hours ago

Thanks for elaborating on the distinction. User defined type guards can get you some of the way there to distinguishing "int

int", but you don't get it for free-- the reality of being a superset of JavaScript?. https://gist.github.com/RikkiGibson/74fa3dbfdb1b2d7ab86d

reply

shados 3 hours ago ... TypeScript? definitely got the structural checking of interfaces right, but I beleive (correct me if I'm wrong, I'm referring to https://github.com/Microsoft/TypeScript/issues/202) that classes are also structurally checked. Flow does nominal checking for those, with very good reasons.

While it's a shame the details are light because you kind of need the presenter to go with the slides, the following explains a few of the reasons between TypeScript? vs Flow:

http://www.scs.stanford.edu/16wi-cs240h/slides/fb-slides.html#(45)

(not the whole deck, just a few slides after 45)

 spicyj 20 hours ago

For comparison, Flow supports tagged unions like this:

http://flowtype.org/blog/2015/07/03/Disjoint-Unions.html

reply

Arnavion 19 hours ago

TS has string types starting from 1.8, although they can't be used for narrowing down the type yet in the way that Flow can.

http://bit.ly/1LhA5id

reply


haskell reflection on types:

import Data.Typeable let x = 5 :: Int typeOf x

---

type erasure vs reified generics, expressiveness and compatibility:

Scala.net didn't die because it was academic. It died due to lack of interest, as nobody cared about a Scala for .NET

reply

dragonwriter 17 hours ago

ISTR a significant reason it died was the .Net platform's reified generics, which made making a language with generics and a type system more expressive than the underlying platform problematic, and especially made it difficult to have something that would be fully compatible with Scala-on-the-JVM.

reply

bad_user 10 hours ago

That's not really true. Yes there are challenges with reified generics and yes Scala's generics don't fit. However you can work around it by doing the type erasure yourself. You can always consider a List[Int] to be a List[Any] and be done with it. And yes that's going to generate inefficient code, but ClojureCLR? doesn't seem to mind.

No, the reason for why Scala.Net didn't happen is because nobody cared. To find proof of this, you only need to look at Clojure. Its .NET implementation is well maintained by David Miller, yet it's very unpopular. And the reason for why .NET developers don't care is because they don't have an open source culture. Or in other words, if it doesn't come from Microsoft, then it doesn't exist.

reply

dragonwriter 3 hours ago

If you do erasure, then you can't also have the level of platform integration Scala has on the JVM: Scala on .NET either ends up as a different-but-similar language that isn't 100% compatible with Scala-on-JVM on a language level (as well the library differences), or its a second-class citizen that doesn't integrate well with the .NET platform, in which case, why have it?

So, in a sense, no on cared -- because neither of the available options was anything anyone wanted.

reply

incepted 13 hours ago

Exactly.

It died for technical reasons because .net supports reified generics, which made it pretty much unable to support Scala's type system.

People who keep saying that erased generics is a stupid idea have no idea what they're talking about.

scala-native is facing insurmountable difficulties, the kind that will certainly not be conquered by a single student who will stop working on it as soon as he graduates.

reply

---

Rusts' designers struggle with making typeclasses modular:

https://mail.mozilla.org/pipermail/rust-dev/2012-July/002047.html : a proposal to constrain the choice of interface implementations somehow, and someone argues against it as too restrictive, and in response pcwalton mentions what he here calls the 'hash table problem' and later calls the 'coherence problem': what if "if I instantiate a hash table and call insert() with the trait instantiated for str with FastHash?, then I might pass that hash table to someone else who calls get() with the trait instantiated for str at QuickHash?."

http://pcwalton.github.io/blog/2012/05/28/coherence/ : pcwalton formally defines three properties of typeclass systems:

(Haskell typeclasses are coherent and extensible but not modular)

He claims that the Rust draft at the time of writing was not coherent, and offers a proposal for coherency. I don't know what the final Rust design was, but https://news.ycombinator.com/item?id=11782286 suggests that it is 'coherent'.

---

"

null and undefined are two of the most common sources of bugs in JavaScript?. Before TypeScript? 2.0, null and undefined were in the domain of every type. That meant that if you had a function that took a string, you couldn’t be sure from the type alone of whether you actually had a string – you might actually have null.

In TypeScript? 2.0, the new --strictNullChecks flag changes that. string just means string and number means number.

let foo: string = null; Error!

What if you wanted to make something nullable? Well we’ve brought two new types to the scene: null and undefined. As you might expect, null can only contain null, and undefined only contains undefined. They’re not totally useful on their own, but you can use them in a union type to describe whether something could be null/undefined.

let foo: string

null = null; Okay!

Because you might often know better than the type system, we’ve also introduced a postfix ! operator that takes null and undefined out of the type of any expression.

declare let strs: string[]

undefined;

Error! 'strs' is possibly undefined. let upperCased = strs.map(s => s.toUpperCase());

'strs!' means we're sure it can't be 'undefined', so we can call 'map' on it. let lowerCased = strs!.map(s => s.toLowerCase()); "

---

got:

Subject: haha I kinda want this

http://www.dx.com/p/neje-fj0002-1-cartoon-3d-cat-style-plush-pillow-cushion-gray-multicolor-362043#.VvwjHT_viiU

---

http://blog.jonathanoliver.com/golang-has-generics/

--- " TypeScript?'s main focus is IDE tooling, not correctness. Here is an example on how generics are unsound in TypeScript?: http://djcordhose.github.io/flow-vs-typescript/2016_hhjs.htm...

If you want to write JavaScript? with a type system focused on soundness, you should give [flow](https://flowtype.org/) a try. "

https://news.ycombinator.com/item?id=12105671

---

hmm the way i am currently defining types in proj-oot-ootAssemblyNotes9 suggests an interesting simple type system:

There are various 'types'. Types can be subtypes and supertypes of other types (a type may have multiple supertypes). Non-concrete types are called 'abstract'. Functions can specify signatures whose inputs and outputs are assigned types.

So these are like Java interfaces and Haskell typeclasses in that you can take any existing type and add new functions to it. They have multiple inheritance.

Now some of these are 'concrete' types, eg INT16 which is like C's "short int". They are associated with a set of 'immediate values'. The set of values that an abstract type has can be induced by recursively finding all of its concrete subtypes, but since more subtypes may be added later, this is subject to change.

Can you add a subtype under an existing concrete type? This would mean that that concrete type's induced values could be larger than its immediate values.

if not, i suppose our 'concrete types' are like haskell's 'types' and our 'abstract types' are like haskell's 'typeclasses'. But the syntax is easier if we consider both of these as different kinds of 'types'.

Eg in Haskell you have special syntax for type 'constraints' and type 'contexts' (typeclass superclasses) in type signatures eg

(==) :: (Eq a) => a -> a -> Bool

instead we define a type 'Eq' and we just say

(==) :: Eq -> Eq -> Bool

note that the semantics there are slightly different, as Haskell (i think) is requiring that there is some actual type that is the same for both arguments, whereas our alternative is not. Is there a way to say what we're saying in Haskell? If so, then Haskell's system is more expressive (b/c it would allow us to, say, have a type error if you try to compare a string and a number).

---

hmm so how would you do what we just did in Haskell?

i guess in Haskell you could do

(==) :: (Eq a, Eq b) => a -> b -> Bool

if you wanted to be able to compare strings and integers

---

And how could we have a system that let's us also express what Haskell's while Haskell did just there? Does this make a merger of 'types' and 'typeclasses' infeasible?

ok after a few minutes of thought:

yeah, Haskell's system is best. It allows you to express both the signature

(==) :: (Eq a) => a -> a -> Bool

but also

(==) :: (Eq a, Eq b) => a -> b -> Bool

(it may be hard to see how to implement the latter; consider

(+) :: (Num a, Num b, Num c) => a -> b -> c

; giving an implementation of that means giving promotion rules

actually promotion rules could be pretty simple eg:

(+) :: (Num a, Num b, Num c) => a -> b -> c (+) :: Int16 -> Int16 -> Int16 (...) (+) :: Int32 -> Int32 -> Int32 (...) (+) :: Int32 -> Int16 -> Int32 (...) (+) :: Int16 -> Int32 -> Int32 (...) (+) :: Num -> Num -> Float32 return Nil

in other words, this gives an implementation for Int16; for Int32; for each combination of Int16 and Int32; and then lastly gives a default for any combination of subclasses of Num that haven't been defined yet. The specific ones take priority over the default by the rule that specifics take priority over superclasses (like Haskell does, i think).

)

so each type signature should really be something like Haskell's, where both type variables and type constraints are explicit. Of course, syntactically, a typeclass or type could be used as shorthand, eg integer addition:

(+) :: (Int a, Int b, Int c) => a -> b -> c

could be written

(+) :: Int -> Int -> Int

and

(+) :: Num -> Num -> Num

could mean

(+) :: (Num a, Num b, Num c) => a -> b -> c

(or it could be shorthand for

(+) :: (Num a) => a -> a -> a

, we'd have to choose)

Types and typeclasses (or, concrete and abstract types) in that, for example, the constraint (Num a) means that the type variable 'a' means some specific type in the typeclass 'Num'; 'a' cannot mean, for example, a sub-typeclass of Num; eg

(==) :: (Eq a) => a -> a -> Bool

cannot be satisfied if the two inputs are different concrete types, even if both of these concrete types appear in some proper sub-typeclass of Eq.

I guess the sense in which types and typeclasses are unified is just that they are the same syntactic place in type constraints:

(Eq a) or (Int a) both seem good (although in Haskell, with Int, you would just omit the type variable and constraint notation and use Int in place of the type variable; but that's just syntax).

---

not sure if this is important:

jballanc 1 day ago [-]

Up until now it's been the realm of PL research. The Ptolemy language is one example I know of: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.86.... [PDF]

If you're familiar with duck typing, behavioral typing is (in essence) the reification of duck typing in a concrete type system. In other words, instead of specifying the type of your argument as "Array", you could specify "some type that is indexable, iterable, and can be appended to".

In Julia (mind you this was just the idea I saw being considered), today you would do:

    function foo(myarray::AbstractArray)
      ...
    end

but in the future you might be able to do something like:

    function foo(myarray::ANY{getindex(), setindex(), iterate(), append()})
      ...
    end

what's really neat, though, is combining this with type aliases, you could have:

    typealias Arraylike ANY{getindex(), setindex(), iterate(), append()}
    function foo(myarray::Arraylike)
      ...
    end

reply

SatvikBeri? 1 day ago [-]

Unless I'm mistaken, this seems to already be available in Scala and is called "structural typing"[0]. Is there a substantial difference?

[0]: https://dzone.com/articles/duck-typing-scala-structural

reply

jballanc 21 hours ago [-]

The difference between structural typing and behavioral typing is subtle. In Scala, you're essentially asking the type system to check for the presence of a member function on the object with a specific type signature. Since the function is contained within the object, you're still only typing based on the object's structure (hence: structural typing).

In Julia, objects are data-only and methods are defined at a module level. So, whereas Scala's structural typing need only introspect the object being passed as an argument, Julia's behavioral typing requires introspection of the entire dispatch tree. The benefit to behavior typing and Julia's multi-dispatch is that if you are missing one or two methods for some type in order to be able to use it in some function, you can always define the missing methods locally.

reply

SatvikBeri? 20 hours ago [-]

Great explanation, thank you.

reply

---

C++ vs C# and Java:

" In C# and Java, the generics system needs to know what methods are available for a class, and it needs to pass this down to the virtual machine. The only way to tell it this is by either hard-coding the actual class in, or using interfaces. For example:

string addNames<T>( T first, T second ) { return first.Name() + second.Name(); }

That code won't compile in C# or Java, because it doesn't know that the type T actually provides a method called Name(). You have to tell it - in C# like this:

interface IHasName?{ string Name(); }; string addNames<T>( T first, T second ) where T : IHasName? { .... }

And then you have to make sure the things you pass to addNames implement the IHasName? interface and so on. The java syntax is different (<T extends IHasName?>), but it suffers from the same problems. ...

C++ suffers from none of these problems. The compiler doesn't care about passing types down to any VM's - if both your objects have a .Name() function, it will compile. If they don't, it won't. Simple. "

"

"

C++ rarely uses the “generics” terminology. Instead, the word “templates” is used and is more accurate. Templates describes one technique to achieve a generic design.

C++ templates is very different from what both C# and Java implement for two main reasons. The first reason is that C++ templates don't only allow compile-time type arguments but also compile-time const-value arguments: templates can be given as integers or even function signatures. This means that you can do some quite funky stuff at compile time, e.g. calculations:

template <unsigned int N> struct product { static unsigned int const VALUE = N * product<N - 1>::VALUE; };

template <> struct product<1> { static unsigned int const VALUE = 1; };

Usage: unsigned int const p5 = product<5>::VALUE;

This code also uses the other distinguished feature of C++ templates, namely template specialization. The code defines one class template, product that has one value argument. It also defines a specialization for that template that is used whenever the argument evaluates to 1. This allows me to define a recursion over template definitions. I believe that this was first discovered by Andrei Alexandrescu.

Template specialization is important for C++ because it allows for structural differences in data structures. Templates as a whole is a means of unifying an interface across types. However, although this is desirable, all types cannot be treated equally inside the implementation. C++ templates takes this into account. This is very much the same difference that OOP makes between interface and implementation with the overriding of virtual methods.

C++ templates are essential for its algorithmic programming paradigm. For example, almost all algorithms for containers are defined as functions that accept the container type as a template type and treat them uniformly. Actually, that's not quite right: C++ doesn't work on containers but rather on ranges that are defined by two iterators, pointing to the beginning and behind the end of the container. Thus, the whole content is circumscribed by the iterators: begin <= elements < end.

Using iterators instead of containers is useful because it allows to operate on parts of a container instead of on the whole.

Another distinguishing feature of C++ is the possibility of partial specialization for class templates. This is somewhat related to pattern matching on arguments in Haskell and other functional languages. For example, let's consider a class that stores elements:

template <typename T> class Store { … }; (1)

This works for any element type. But let's say that we can store pointers more effciently than other types by applying some special trick. We can do this by partially specializing for all pointer types:

template <typename T> class Store<T*> { … }; (2)

Now, whenever we instance a container template for one type, the appropriate definition is used:

Store<int> x; Uses (1) Store<int*> y; Uses (2) Store<string> z; Uses (2), with T = string*.

share

edited Oct 19 '11 at 1:29 Mankarse 26.8k551110

answered Aug 28 '08 at 7:11 Konrad Rudolph 310k73640891

I've sometimes wished the generics feature in .net could allow things besides types to be used as keys. If value-type arrays were a part of the Framework (I'm surprised they're not, in a way, given the need to interact with older APIs that embed fixed-sized arrays within structures), it would be useful to declare a class which contained a few individual items and then a value-type array whose size was a generic parameter. As it is, the closest one can come is to have a class object which holds the individual items and then also holds a reference to a separate object holding the array. – supercat Jan 6 '13 at 18:20

@supercat If you interact with legacy API the idea is to use marshalling (which can be annotated via attributes). The CLR doesn’t have fixed-size arrays anyway so having non-type template arguments would be of no help here. – Konrad Rudolph Jan 6 '13 at 19:27

I guess what I find puzzling is that it would seem like having fixed-sized value-type arrays shouldn't have been hard, and it would have allowed many data types to be marshalled by reference rather than by value. While marshal-by-value can be useful in cases that genuinely can't be handled any other way, I would regard marshal-by-ref to be superior in nearly all cases where it's usable, so allowing such cases to include structs with fixed-sized arrays would have seemed a useful feature. – supercat Jan 6 '13 at 20:35

BTW, another situation where non-type generic parameters would be useful would be with data types that represent dimensioned quantities. One could include dimensional information within instances that represent quantities, but having such information within a type would allow one to specify that a collection is supposed to hold objects representing a particular dimensioned unit. – supercat Jan 6 '13 at 20:39 "

"

Follow-up to my previous posting.

Templates are one of the main reasons why C++ fails so abysmally at intellisense, regardless of the IDE used. Because of template specialization, the IDE can never be really sure if a given member exists or not. Consider:

template <typename T> struct X { void foo() { } };

template <> struct X<int> { };

typedef int my_int_type;

X<my_int_type> a; a.

Now, the cursor is at the indicated position and it's damn hard for the IDE to say at that point if, and what, members a has. For other languages the parsing would be straightforward but for C++, quite a bit of evaluation is needed beforehand.

It gets worse. What if my_int_type were defined inside a class template as well? Now its type would depend on another type argument. And here, even compilers fail.

template <typename T> struct Y { typedef T my_type; };

X<Y<int>::my_type> b;

After a bit of thinking, a programmer would conclude that this code is the same as the above: Y<int>::my_type resolves to int, therefore b should be the same type as a, right?

Wrong. At the point where the compiler tries to resolve this statement, it doesn't actually know Y<int>::my_type yet! Therefore, it doesn't know that this is a type. It could be something else, e.g. a member function or a field. This might give rise to ambiguities (though not in the present case), therefore the compiler fails. We have to tell it explicitly that we refer to a type name:

X<typename Y<int>::my_type> b;

Now, the code compiles. To see how ambiguities arise from this situation, consider the following code:

Y<int>::my_type(123);

This code statement is perfectly valid and tells C++ to execute the function call to Y<int>::my_type. However, if my_type is not a function but rather a type, this statement would still be valid and perform a special cast (the function-style cast) which is often a constructor invocation. The compiler can't tell which we mean so we have to disambiguate here.

"

-- http://stackoverflow.com/questions/31693/what-are-the-differences-between-generics-in-c-sharp-and-java-and-templates-i

" Bruce Eckel: How do C# generics compare with C++ templates?

Anders Hejlsberg: To me the best way to understand the distinction between C# generics and C++ templates is this: C# generics are really just like classes, except they have a type parameter. C++ templates are really just like macros, except they look like classes.

The big difference between C# generics and C++ templates shows up in when the type checking occurs and how the instantiation occurs. First of all, C# does the instantiation at runtime. C++ does it at compile time, or perhaps at link time. But regardless, the instantiation happens in C++ before the program runs. That's difference number one. Difference number two is C# does strong type checking when you compile the generic type. For an unconstrained type parameter, like List<T>, the only methods available on values of type T are those that are found on type Object, because those are the only methods we can generally guarantee will exist. So in C# generics, we guarantee that any operation you do on a type parameter will succeed.

C++ is the opposite. In C++, you can do anything you damn well please on a variable of a type parameter type. But then once you instantiate it, it may not work, and you'll get some cryptic error messages. For example, if you have a type parameter T, and variables x and y of type T, and you say x + y, well you had better have an operator+ defined for + of two Ts, or you'll get some cryptic error message. So in a sense, C++ templates are actually untyped, or loosely typed. Whereas C# generics are strongly typed. " -- [4]

---

how to say things: do we say that we 'ascribe' a type to a variable? these guys do: [5]

---

Occurrence typing:

https://docs.racket-lang.org/ts-guide/occurrence-typing.html

"

...if Typed Racket can determine the type a variable must have based on a predicate check in a conditional expression, it can narrow the type of the variable within the appropriate branch of the conditional....

To illustrate, consider the following code:

    (: flexible-length (-> (U String (Listof Any)) Integer))
    (define (flexible-length str-or-lst)
      (if (string? str-or-lst)
          (string-length str-or-lst)
          (length str-or-lst)))...

Typed Racket successfully type-checks this function because the type system understands that in the "then" branch of the if expression, the predicate string? must have returned a true value. The type system further knows that if string? returns true, then the str-or-lst variable must have type String and can narrow the type from its original union of String and (Listof Any).

...

This may raise the question: how does Typed Racket know how to narrow the type based on the predicate?

The answer is that predicate types in Typed Racket are annotated with logical propositions that tell the typechecker what additional information is gained when a predicate check succeeds or fails.

For example, consider the REPL’s type printout for string?:

    > string?
  1. <procedure:string?>

...

5.4 A caveat about set!

If a variable is ever mutated with set! in the scope in which it is defined, Typed Racket cannot use occurrence typing with that variable. This precaution is needed to ensure that concurrent modification of a variable does not invalidate Typed Racket’s knowledge of the type of that variable. Also see Guidelines for Using Assignment.

Furthermore, this means that the types of top-level variables in the REPL cannot be refined by Typed Racket either. This is because the scope of a top-level variable includes future top-level interactions, which may include mutations. It is possible to work around this by moving the variable inside of a module or into a local binding form like let.

"

---

'inhabited' is the word i was looking for; a type is 'inhabited' by values

---

Python Copperhead types, summary:

---

http://mypy.readthedocs.io/en/latest/cheat_sheet.html

---

clusmore 1 day ago [-]

Honestly I haven't looked into MyPy? a huge amount, and haven't used it yet. But from reading the docs on it I feel like it's taking the wrong approach. In my opinion, Python is all about duck typing, so having a static type checker that seems to focus on concrete types feels wrong to me.

Consider the first example,

  def sum_and_stringify(nums: List[int]) -> str:
      return str(sum(nums))

The type here is way more specific than it needs to be. Not only will this work on any sequence type (anything that supports __iter__), the element type only needs to support __add__ and __radd__ (to work against the implicit seed value of sum).

I really feel like in order to get the best of duck typing, you need a good syntax for describing types by usage, not by explicit name. Please let me know if I'm missing something, and this is actually more expressive than the documentation suggests.

reply

dbcurtis 1 day ago [-]

Well, I like to put that another way -- I think Python is all about protocols (in the Python sense of the word protocol). I think that is what most people mean when they say Python is all about duck typing, and it communicates the concept more precisely.

The concept of 'type' is overloaded with too many meanings these days. It started out as a what-storage-to-allocate and which-instruction-to-generate (int v float) concept (FORTRAN I, variables starting with I..N are ints, others real). Deep class hierarchies muddied the waters by overlaying the idea of whether or not a class implements a particular property or method, and how to locate the property or method that you want.

Python shows us that types and protocols/interfaces are two very different thing. In Python, asking 'isinstance()' is usually a bad idea unless you are doing something very low level, low level as in next stop is a C extension. The missing predicate in Python is 'hasprotocol()'. Abstract base classes can be used to accomplish that: isinstance(foo, SomeABC?), but I think the intent could be more transparent with different syntax.

reply

---

" OCaml with its structurally typed object system with inferred types. For example:

  1. let f obj x y = (obj#m x)#n y;; val f : < m : 'a -> < n : 'b -> 'c; .. >; .. > -> 'a -> 'b -> 'c = <fun>

Here I defined a function taking 3 arguments, called method m on obj, passing x as argument, then called method n on the result of that, passing y as argument.

Note the inferred type signature for this: the first argument is of type <m : 'a -> <n : 'b -> 'c; ..>; ..> - i.e. any object that has a method named m (and possibly some other unspecified members - that's what ".." means), with said method m having a signature that allows us to pass some 'a, and returning another object of type <n : 'b -> 'c; ..> - i.e. something with a method named n that accepts 'b and returns 'c. 'a and 'b' are then used as types of x and y, respectively, and 'c is the the result of f. " -- [6]

---

dom96 18 hours ago [-]

> I really feel like in order to get the best of duck typing, you need a good syntax for describing types by usage, not by explicit name.

Not sure if this is of interest to you, but the Nim[1] programming language offers a feature that allows you to do exactly what you described. It is called concepts and is documented here: http://nim-lang.org/docs/manual.html#generics-concepts

As a bonus, Nim is also quite Python-like.

1 - http://nim-lang.org

reply

clusmore 18 hours ago [-]

Yep that sounds like what I mean. Haskell typeclasses, Go interfaces, TypeScript? interfaces are further examples. Not Java/C# interfaces though, as they need to be declared at design time, and you can't force existing classes to implement interfaces they haven't already declared themselves as implementing.

reply

---

nim concepts:

" Concepts, also known as "user-defined type classes", are used to specify an arbitrary set of requirements that the matched type must satisfy.

Concepts are written in the following form:

type Comparable = concept x, y (x < y) is bool

  Container[T] = concept c
    c.len is Ordinal
    items(c) is T
    for value in c:
      type(value) is T"

---

" Here is a little list of drawbacks of static type systems with features like you describe (parametric types, ADTs...): Type dependency hell (banana, monkey, jungle, etc), having to fight/convince the type inferencer to accept any but the simplest things, having to type many things twice.

Looking at Haskell, "almost everything is inferred" is a lie in my experience. You are encouraged to write code using higher-order and highly parametric functions. If you do, the error messages you'll get if you don't annotate are plain sick. A "

[7]

tigershark 21 hours ago [-]

You cannot do any kind of Domain Driven Design with dynamic typing. In F# you can have a type email address and it will be impossible to pass an unverified string there. It has to be a valid email address, and you will know it at compile time. Good luck to try to achieve the same effect in python without writing tons and tons of useless tests just to check the type. And if you can keep all the type of your system in your head I don't think you ever worked in a real system.

reply

jstimpfle 17 hours ago [-]

I have gone that route in Haskell and it was a mess. In the end you need to extract the string again (basically everytime you do something meaningful with it). All these pattern matches kill code readability/writeability.

Also, in Haskell one needs to encapsulate the real constructor in its own module to make sure the data is only constructed through a sanitizing constructor. That's quite some overhead (and makes pattern matching impossible).

What might be useful instead is first class "tags". In Perl6, you can subset types to values that match a condition (for example, strings that match an email regex (cough)). They are still strings so can be used unchanged with other functionality that does not need the tag. It seemed quite usable to me (applications are limited, though). However the creator said it's still expensive because they haven't figured out / implemented how to transfer invariants, so they are checked at each function boundary.

In Python, you can use duck typing: subclass str, it's a dirty hack but works very nicely.

---

i don't understand the last comment here:

minitech 1 day ago [-]

You’re making out having to explicitly specify a type when type inference doesn’t do a satisfactory job as some kind of extremely painful thing, but it’s not. You just define the type of your object, which is something you had to know anyways; now it’s written down and people reading don’t have to guess at or remember what it is.

reply

jstimpfle 1 day ago [-]

Annotating even the last bit of code that uses type class methods until the error message becomes clear is very cumbersome. For example, I can't say (traverse :: The List instance), but have to dig out the whole annoying signature, or go look for a more strategic value where the same information can be put in fewer characters. For another thing, it often duplicates the amount of lines needed (or more if you like to put in whitespace before types). It's definitely very annoying.

reply

dllthomas 20 hours ago [-]

> I can't say (traverse :: The List instance)

Actually, in GHC 8.0 you can do exactly that, with the TypeApplictions? extension.

    Prelude> :set -XTypeApplications
    Prelude> :t traverse @[]
    traverse @[] :: Applicative f => (a -> f b) -> [a] -> f [b]

reply

---

jstimpfle 1 day ago [-]

I will think about it, but would probably not be comfortable with it.

For now a few words that I hope I won't regret later (apart from the things I mentioned): The bulk of invariants / assertions in many real-life programs can't be expressed with mainstream type systems at all. They are too specific or only come to life dynamically. Things like: This array of integers is sorted ascendingly, and that index is a valid index into this other array which points to a number between 48 and 58. Or this table's column over there contains only values that are also present in that other table that just happens to be present now (but must be expunged from working memory after the next subtask). Checking if an integer fits in 8 bits and then converting to a byte is no safer in Haskell than in any other language.

So much to put the usefulness of mainstream types for static correctness in relation.

Now much of the tinkering that is going on in Haskell projects seems to be shoehorning yet one more real-world invariant in another crazy type. Maybe the next brilliant idea works for one more toy case in the end. Great, but the cost/benefit ratio is just bad.

I think the most important thing in software architecture is modularity, because the most pressing need in software development is the need for change. If my project is very modular, it's sufficient to have clear entry points to each module with very simple data types in the signature. The internals can be a dirty hack and rewritten later, or the module thrown away when the idea turns out bad. Interfaces on the other hand can't be changed as easily since they affect much more code. So a good approach is making interfaces that accept tables, augmented by a textual description of invariants so the user easily "gets" the meaning of the data and can reshape/preprocess the data as needed. This enables isolated rewrites of modules. It also enables creative use of data in unforeseen ways. Clever types on the other hand have a very strong influence not only on the design of module interfaces but also on the dependent modules' implementations, because 1) it's more cumbersome to reshape complex structures in a way suitable for clean implementation, and 2) because type systems can't usually transfer invariants to reshaped representations (and after all the goal was to let the compiler handle the invariants, so reshaping is a no-go).

In short, complex types _kill_ modularity because they have far too much influence on data layout.

---

porker 18 hours ago [-]

> Most of my code now is structured as tables, which greatly simplifies many transformations. There is no pressing need for typing tables, and anyway most of these type systems really suck at "tables transformation algebra".

What do you mean by "tables"? I think of a database table of rows/columns, or a matrix.

reply

jstimpfle 18 hours ago [-]

Exactly. Arrays of C structures. Python lists of (named?) tuples. Mathematically, simple relations.

It helps if the language supports creation of indices / reshaping (table joins, filters, making hierarchies).

reply

---

massysett 1 day ago [-]

I can already mix static and dynamic types. Use Haskell. With Data.Dynamic you get all the dynamic types you want.

reply

---

" We aim to define a useful type system that will help programmers catch runtime exceptions, but we want it to be usable and easy-going. That is why:

    Nil is not a value of every type T. You need to use unions of T | Nil (or T?)
    Array(T) is able to hold only one type (although it can be a union), but we don’t know which indices are valid in compile time.
    Tuples(*T) are not as flexible as an Array(T) but given a literal we can know if it is a valid index and which type it corresponds to in compile time.
    Array(T)/Tuple(*T) relationship is analogous to Hash(K,V)/NamedTuple(**T).
    Array(T?)#compact returns an Array(T)"

-- [8]

---

kalkin 13 hours ago

parent flag favorite on: 2017 Rust Roadmap

Speaking of "guaranteed not to allocate", is there a way that you could express that in a type? Seems like that might be nice to have.

killercup 3 hours ago [-]

Not in the type system itself, but you could write a lint to forbid heap allocation. This way, you could annotate a function (with e.g. `#[forbid(allocations)]`) to get a compile error when your function (or code your function calls) tries to allocate. This might not be easy, though :)

reply

tatterdemalion 13 hours ago [-]

Not in Rust's type system. In a pure language, you could have some sort of "Heap" monad similar to the "IO" type in Haskell.

reply

---

 chriswarbo 11 hours ago | unvote [-]

I do have some sympathy for the author's desire to have record extension (re-)added, as that looks like a pure win, from my outside perspective. Maybe there are concerns which insiders may be better able to spot, like losing some reasoning ability.

As for typeclasses, I think Elm's stance is perfectly reasonable. Typeclasses aren't a pure win, they have downsides too:

There are probably more issues in the literature, but these are ones I've been banging my head against recently.

Typeclasses are a great idea and a useful addition to the PLT toolbox, but including them in a language isn't an automatic improvement: it's more of a design choice to steer the language down a particular path, when other languages may prefer other paths. Similar to using strict/non-strict evaluation, or exceptions, or macros.

reply

maxthegeek1 3 hours ago [-]

Record extension was removed because it allowed Evan to improve error messages, and because he found that Elm's power users didn't use the feature.

reply

---

a complaint about Elm having neither typeclasses nor syntax for record extension:

http://reasonablypolymorphic.com/blog/elm-is-wrong#fn1

---

"When I say the language is broken, look at Go type system, then look at how Go reflection makes the language look a dynamically typed one. It would have been smarter to tone down the reflection and make it unnecessary with a smarter type system. "

"Would be curious to hear what "safety" you're referring to, is it just that it has a basic static type system, (which is constantly being undermined by interface{} and reflection), or is there more to it?"

---

"

AsyncAwait? 1 day ago [-]

> strikes the right balance for me between productivity and safety.

Would be curious to hear what "safety" you're referring to, is it just that it has a basic static type system, (which is constantly being undermined by interface{} and reflection), or is there more to it?

Genuinely curious.

reply

chmike 23 hours ago [-]

Compared to C it is safer. I never saw a segmentation fault, only some panic errors with bound checking.

I prefer go to python or javascipt. It's far too easy to make errors in them. Minimal static code checking.

reply "

---

" aturon commented on Sep 2

@withoutboats In a nutshell, it means that Rust will not attempt to ensure traditional parametricity for type arguments (i.e. that generic code behaves "equivalently" when instantiated with different types). This is already formally the case due to the ability to get the size of a type parameter, but we're opening the door to observable, behavioral differences under different type arguments.

That means we will permit language features that let you write a function like:

fn print<T>(t: &T) { ... }

which e.g. prints its argument using Display if available, otherwise Debug if available, otherwise prints a generic message. Whereas in today's Rust, you might assume that such a function must behave more "uniformly" for all T (and in fact that it couldn't interact meaningfully with its argument).

The tradeoff is:

    Benefit: additional expressiveness, of course. In particular, in the specialization thread I and others argued that this kind of "static reflection" is essential for reaching true zero-cost abstraction. A possible counter-argument: it could be treated as an unsafe feature, where marking as safe requires ensuring that there's no "observable" difference in behavior, just better performance. But of course there are use cases like print above where different behavior is the whole point. See the specialization thread for more.
    Downside: the signature of a function tells you less about that function's behavior. That is, you can make certain assumptions about a signature like print in Rust today, e.g. that it cannot access anything "inside" its argument -- and that reasoning would be invalidated. Counter-argument: in almost all cases you need a contract for a function that goes beyond what the types say anyway; if this kind of lack of reflection is important, just make it an explicit part of the function's contract. In particular, the vast majority of generic functions will still behave parametrically, and those that don't are likely to be fairly obvious or otherwise marked.

Note that all of the above is specific to type parameters. Lifetime parameters, on the other hand, are intended to remain parametric -- e.g. you can't change the behavior of your function depending on whether a given lifetime is 'static or not. That's important for functions like Ref::map.

"

---

"In a Tale of Three Safeties, we discussed three kinds of safety: type, memory, and concurrency" -- http://joeduffyblog.com/2016/11/30/15-years-of-concurrency/

---

https://github.com/prayerslayer/js.spec/blob/master/README.md

---

https://blogs.msdn.microsoft.com/typescript/2016/12/07/announcing-typescript-2-1/ :

" keyof and Lookup Types

Many libraries take advantage of the fact that objects are (for the most part) just a map of strings to values. Given what TypeScript? knows about each value’s properties, there’s a set of known strings (or keys) that you can use for lookups.

That’s where the keyof operator comes in.

interface Person { name: string; age: number; location: string; }

let propName: keyof Person;

The above is equivalent to having written out

let propName: "name"

"age""location";

This keyof operator is actually called an index type query. It’s like a query for keys on object types, the same way that typeof can be used as a query for types on values.

The dual of this is indexed access types, also called lookup types. Syntactically, they look exactly like an element access, but are written as types:

interface Person { name: string; age: number; location: string; }

let a: Person["age"];

This is the same as saying that n gets the type of the age property in Person. In other words:

let a: number;

When indexing with a union of literal types, the operator will look up each property and union the respective types together.

Equivalent to the type 'string

let nameOrAge: Person["name"
number'
"age"];

This pattern can be used with other parts of the type system to get type-safe lookups, serving users of libraries like Ember.

function get<T, K extends keyof T>(obj: T, propertyName: K): T[K] { return obj[propertyName]; }

let x = { foo: 10, bar: "hello!" };

let foo = get(x, "foo"); has type 'number' let bar = get(x, "bar"); has type 'string'

let oops = get(x, "wargarbl"); error!

"

---

" Mapped Types

Mapped types are definitely the most interesting feature in TypeScript? 2.1.

Let’s say we have a Person type:

interface Person { name: string; age: number; location: string; }

Much of the time, we want to take an existing type and make each of its properties entirely optional. With Person, we might write the following:

interface PartialPerson? { name?: string; age?: number; location?: string; }

Notice we had to define a completely new type.

Similarly, we might want to perform a shallow freeze of an object:

interface FrozenPerson? { readonly name: string; readonly age: number; readonly location: string; }

Or we might want to create a related type where all the properties are booleans.

interface BooleanifiedPerson? { name: boolean; age: boolean; location: boolean; }

Notice all this repetition – ideally, much of the same information in each variant of Person could have been shared.

Let’s take a look at how we could write BooleanifiedPerson? with a mapped type.

type BooleanifiedPerson? = { [P in "name"

};
"age""location"]: boolean

Mapped types are produced by taking a union of literal types, and computing a set of properties for a new object type. They’re like list comprehensions in Python, but instead of producing new elements in a list, they produce new properties in a type.

In the above example, TypeScript? uses each literal type in "name"

"age""location", and produces a property of that name (i.e. properties named name, age, and location). P gets bound to each of those literal types (even though it’s not used in this example), and gives the property the type boolean.

Right now, this new form doesn’t look ideal, but we can use the keyof operator to cut down on the typing:

type BooleanifiedPerson? = { [P in keyof Person]: boolean };

And then we can generalize it:

type Booleanify<T> = { [P in keyof T]: boolean };

type BooleanifiedPerson? = Booleanify<Person>;

With mapped types, we no longer have to create new partial or readonly variants of existing types either.

Keep types the same, but make every property optional. type Partial<T> = { [P in keyof T]?: T[P]; };

Keep types the same, but make each property to be read-only. type Readonly<T> = { readonly [P in keyof T]: T[P]; };

Notice how we leveraged TypeScript? 2.1’s new indexed access types here by writing out T[P].

So instead of defining a completely new type like PartialPerson?, we can just write Partial<Person>. Likewise, instead of repeating ourselves with FrozenPerson?, we can just write Readonly<Person>! "

---

https://blogs.msdn.microsoft.com/typescript/2016/12/07/announcing-typescript-2-1/

" Partial, Readonly, Record, and Pick

Originally, we planned to ship a type operator in TypeScript? 2.1 named partial which could create an all-optional version of an existing type. This was useful for performing partial updates to values, like when using React‘s setState method to update component state. Now that TypeScript? has mapped types, no special support has to be built into the language for partial.

However, because the Partial and Readonly types we used above are so useful, they’ll be included in TypeScript? 2.1. We’re also including two other utility types as well: Record and Pick. You can actually see how these types are implemented within lib.d.ts itself. "

---

http://www.w3schools.com/js/js_syntax.asp says the most important types are Number and String

---

why rust doesn't have purity annotations anymore:

https://mail.mozilla.org/pipermail/rust-dev/2013-April/003926.html

what rust's purity annotations used to look like:

http://smallcultfollowing.com/babysteps/blog/2012/10/12/extending-the-definition-of-purity-in-rust/

---