How to define a function type of a non-recursive functions that has still a recursive type

Question

Given is a Javascript function like

const isNull = x => x === null ? [] : [isNull];

Such a function might be nonsense, which is not the question, though.

When I tried to express a Haskell-like type annotation, I failed. Likewise with attempting to implement a similar function in Haskell:

let isZero = \n -> if n == 0 then [] else [isZero] -- doesn't compile

Is there a term for this kind of functions that aren't recursive themselves, but recursive in their type? Can such functions be expressed only in dynamically typed languages?

Sorry if this is obvious - my Haskell knowledge (including strict type systems) is rather superficial.

Answer 1

You need to define an explicit recursive type for that.

newtype T = T (Int -> [T])

isZero :: T
isZero = T (\n -> if n == 0 then [] else [isZero])

The price to pay is the wrapping/unwrapping of the T constructor, but it is feasible.

If you want to emulate a Javascript-like untyped world (AKA unityped, or dynamically typed), you can even use

data Value
   = VInt Int
   | VList [Value]
   | VFun (Value -> Value)
   ...

(beware of a known bug)

In principle, every Javascript value can be represented by the above huge sum type. For example, application becomes something like

jsApply (VFun f) v = f v
jsApply _        _ = error "Can not apply a non-function value"

Note how static type checks are turned into dynamic checks, in this way. Similarly, static type errors are turned into runtime errors.

Answer 2

Chi showed how such an infinite type can be implemented: you need a newtype wrapper to “hide” the infinite recursion.

An intriguing alternative is to use a fixpoint formulation. Recall that you could pseudo-define something recursive like your example as

isZero = fix $ \f n -> if n == 0 then [] else [f]

Likewise, the type can actually be expressed as a fixpoint of the relevant functors, namely of the composition of (Int ->) and [] (which in transformer gestalt is ListT):

isZero :: Fix (ListT ((->) Int))
isZero = Fix . ListT $ \n -> if n==0 then [] else [isZero]

Also worth noting is that you probably don't really want ListT there. MaybeT would be more natural if you only ever have zero or one elements. Even more nicely though, you can use the fact that functor fixpoints are closely related to the free monad, which gives you exactly that “possibly trivial” alternative case:

isZero' :: Free ((->) Int) ()
isZero' = wrap $ \n -> if n==0 then Pure () else isZero'

Pure () is just return () in the monad instance, so you can as well replace the if construct with the standard when:

isZero' = wrap $ \n -> when (n/=0) isZero'