c_wraith 2017-03-06 14:47:05
Haskell feels infinite. but that's because ghc keeps advancing. so much to keep learning.
c_wraith 2017-03-06 14:48:42
I just learned that TypeInType allows higher-rank kinds. except they're not called kinds anymore. unless.. Do we still call them kinds?
c_wraith 2017-03-06 14:48:49
type-types?
centril 2017-03-06 14:50:00
c_wraith: kinds were always type of types
centril 2017-03-06 14:50:27
just as you can have types of types of types
lyxia 2017-03-06 14:50:41
kinds become sorts
centril 2017-03-06 14:50:58
(Universe sets in Agda)
centril 2017-03-06 14:51:19
c_wraith: interesting: https://en.wikipedia.org/wiki/Girard%27s_paradox
c_wraith 2017-03-06 14:51:29
my question was more.. if they no longer behave differently, do we still call them something else?
centril 2017-03-06 14:53:01
c_wraith: well... TypeInType makes * :: * , which is an analog to Russel's Paradox... so you can prove bottom thus
Tuplanolla 2017-03-06 14:53:37
It's not `KindInType`, is it now?
centril 2017-03-06 14:54:18
Tuplanolla: call it what you want... but: * :: * is inconsistent as a logic
centril 2017-03-06 14:54:28
but haskell was already inconsistent as a logic, so that is fine
lyxia 2017-03-06 14:59:33
c_wraith: It can still be useful and improve clarity to have a richer vocabulary when talking about a type and its own type.
centril 2017-03-06 14:59:46
lyxia: +1
c_wraith 2017-03-06 15:02:57
centril, haskell was already an inconsistent logic, so it's not like it's worse.
centril 2017-03-06 15:03:19
c_wraith: I already stated that ;)
centril 2017-03-06 15:13:59
hmm.. when using one signature for multiple functions like: a, b, c :: MyType ... can you specify haddok docs on the definitions of the functions ?
lyxia 2017-03-06 15:14:21
nope
centril 2017-03-06 15:14:27
damn
centril 2017-03-06 15:14:31
that sucks
lyxia 2017-03-06 15:17:27
If you try you'll just duplicate the text
