GOPHERSPACE.DE - P H O X Y
gophering on hngopher.com
HN Gopher Feed (2017-07-07) - page 1 of 10
 
___________________________________________________________________
Where Do Type Systems Come From?
34 points by philix001
http://blog.felipe.rs/2017/07/07/where-do-type-systems-come-from/
___________________________________________________________________
 
smcl - 45 minutes ago
I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth
knowledge or opinions on type systems. I get that these underpin
the technology we as programmers use every single day, but I'm a
little ashamed that I can't get excited about the subject and feel
like it's too late for me to bother trying.
 
  agumonkey - 40 minutes ago
  To each his own path. Maybe you'll change course, maybe not,
  maybe type theory will evolve (HoTT comes to mind).
 
    miguelrochefort - 5 minutes ago
    I can't seem to grasp HoTT.Are there any approachable resources
    on the subject?
 
  Kenji - 35 minutes ago
  It's never too late to bother trying. If you think it'll benefit
  you in life, just go for it and study it.
 
    AnimalMuppet - 20 minutes ago
    If.  I suspect that smcl can't get excited about type systems
    because of not seeing the benefit.For me, types are sets of
    possible values, plus sets of valid operations on those values.
    I don't much care where they come from.  As far as I am
    concerned, they are an engineering construct to make
    programming easier and safer, and are interesting only to the
    degree that they accomplish those goals.  Any connection to
    pure math is completely incidental; if there were no such
    connection, it would not make (programming) types any less
    useful.Now, math often gives deeper insight into what's going
    on, and enables you to create more powerful (useful)
    abstractions.  But if the useful abstractions don't correspond
    perfectly to types as used by mathematics, I don't care.
 
  philix001 - 34 minutes ago
  I don't think it's common for programmers to have in depth
  opinions about type systems. And most of the ones who do may not
  really know what they're talking about.
 
  ridiculous_fish - 22 minutes ago
  > I get that these underpin the technology we as programmers use
  every single dayIs this actually true? Of course Haskell, Idris,
  etc. leverage type theory, but how much type theory underlies the
  type systems of widespread practical languages like C# or Java?
  Can something like C++'s SFINAE be grounded in type theory, or is
  it just a hack?
 
  Drup - 18 minutes ago
  I believe you get an actual interest for type systems when you
  start using a rich one. Unfortunately, most mainstream languages
  have very poor type systems. In particular, it will come
  naturally over time if you start using languages like OCaml, F#,
  Scala, Rust, Haskell, ...
 
miguelrochefort - 4 minutes ago
Don't they teach this stuff in school?
 
pier25 - 39 minutes ago
Reminded me of G?del's incompleteness theorems.First incompleteness
theoremAny consistent formal system F within which a certain amount
of elementary arithmetic can be carried out is incomplete; i.e.,
there are statements of the language of F which can neither be
proved nor disproved in F.Second incompleteness theoremFor any
consistent system F within which a certain amount of elementary
arithmetic can be carried out, the consistency of F cannot be
proved in F itself.
 
agumonkey - 39 minutes ago
Types are close to adjoint functors / adjunctions and partial
evaluation. Assigning restricted information to part of a structure
to gain knowledge through limitation (math).
 
simplify - 22 minutes ago
If you haven't thought much about type systems but want to
understand what the big deal is, I wrote a post specifically for
you [1]. It draws motivation for wanting a good static type system
from first principles.[1] https://gilbert.ghost.io/type-systems-
for-beginners-an-intro...
 
threepipeproblm - 17 minutes ago
I loved this because I have read most of the source material in the
context of logic, but never made the lead to type theory in
computer science.
 
zzzcpan - 17 minutes ago
"Even though theoretically, type theories and type systems are not
enough to prevent all the problems in logic and programming, they
can be improved and refined to prevent an increasingly number of
problems in the practice of logic and programming."It's actually
just a belief. Nothing suggests that type systems and type theories
can be improved to be practical at preventing bugs. I'd say it's
the opposite, even with as much understanding about the nature of
bugs as we have today, they don't look very promising, unlikely to
make it even into the top ten of other different approaches.