Re:Confession of a Haskell Hacker
by rpearl on Sunday July 08, 2012 @07:42PM
(#4216087)
Some of them are only inhabited by bottom, no? I cannot write down a function f :: a -> b besides:
[ Parent
| on HN ]
There are a lot of other Haskell features you can use. Term-level recursion works:
f :: a -> b
f = f
Type-level recursion works, even without explicit term-level recursion: data T a b = C (T a b -> (a -> b))
q :: T a b -> (T a b -> (a -> b))
q (C f) = f
w :: T a b -> (a -> b)
w x = (q x) x
f :: a -> b
f = w (C w)
This is basically encoding Russell's paradox at the type level. You can write out f explicitly, just so that it doesn't look like you might somehow still be applying w to itself recursively: g :: a -> b
g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x))
There are even ways of doing this using highly impredicative definitions involving GADTs and type families, without involving any explicit recursion at all:http://okmij.org/ftp/Haskell/impredicativity-bites.html
The GADT example no longer seems to work, so changes to GADT type checking might have eliminated it, but the type family one still does.
Re:Confession of a Haskell Hacker
by applicative on Monday July 09, 2012 @11:55AM
(#4218726)
It doesn't affect your objection to MaleKitten but not all types are occupied in Haskell. You are thinking of kind * By contrast,
{-#LANGUAGE DataKinds#-}
a :: 'Nothing
a = a
and {-#LANGUAGE MagicHash#-}
import GHC.Prim
a :: Int#
a = a
don't typecheck, though I cant say I understand the ins and outs of the latter.