Hacker News new | ask | show | jobs
by rpearl 5092 days ago
Some of them are only inhabited by bottom, no? I cannot write down a function f :: a -> b besides:

    f :: a -> b
    f = undefined
1 comments

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.

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.