Hacker News new | past | comments | ask | show | jobs | submit login

Thank you for pointing me in the direction of MLTT/intuitionism/CT. I have a lot of good processing ahead of me.

One more thought about types. Stereotypes are a usage of types in our thinking. Stereotypes are a relatively low resolution (and low information load) way of defining a person. Stereotypes are a type system to model people.

Type systems seem to be brittle when it comes to increasing/decreasing resolution. It seems like type systems need to become more elaborate to account for these different resolution scopes that combine to ultimately make a concept. Just like imposing a type on an individual, one needs to account for the many nuances of that person. These nuances are sometimes & sometimes not applicable to other people with similar nuances.

One way to look at this is that you have types which classify a structure/theory. In some sense, it works like this—you have generators which allow you to inductively define a large set of "things", then you have laws which cut those things down.

For instance, the theory of monoids gives rise to the generators

    zero : AMonoid
    +    : AMonoid -> AMonoid -> AMonoid
satisfying the laws

    zero + a = a
    a + zero = a
    a + (b + c) = (a + b) + c
Types can be refined and combined in principled ways by glomming the generators and laws together. Ultimately, what you're looking for is a notion of the set generated by all of the generators satisfying all of the laws plus any "coherence" laws which help to define what happens when two laws interact.

Unfortunately, nobody is very good at this today. It's a goal to be able to automatically achieve the above system in such a way that isn't O(n^2) effort to encode.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact