These are chat archives for typelevel/general

18th
Jul 2017
Miles Sabin
@milessabin
Jul 18 2017 08:19
@edmundnoble I think it helps to make a distinction between "dependently typed" and "full-spectrum dependently typed". Scala and Haskell are the former, but not the latter.
If Scala isn't dependently typed in the weaker sense then neither is Dependent ML which would surely be very odd.
Fabio Labella
@SystemFw
Jul 18 2017 10:57
@milessabin where would you say is the turning point that gets a SystemFw based language (well, Scala is not, but I hope my point is clear) into the dependently typed spectrum?
Some form of type families (or in the case of scala, type members + kinda functional dependencies) are a must, but is that enough? Or is it singletons?
Unfortunately I'm not aware of any formal account of this specific debate since the "dependently typed" features of Haskell mostly grew organically (before Richard Eisenberg plan), and Scala has only recently received a more solid theoretical model.
Miles Sabin
@milessabin
Jul 18 2017 11:18
Singletons is more than enough.
Ch. 2 of Advanced Topics in Types and Programming Languages, Dependent Types, Aspinall and Hofmann starts with a fairly broad definition "the terminology 'dependent types' is usually used to indicate a particular class of type-valued functions: those functions which send terms to types".
Miles Sabin
@milessabin
Jul 18 2017 11:23
I'm happy to include both GADTs and OO-style subtyping under that heading.