2

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.

2 Answers2

5

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.

chi
  • 111,837
  • 3
  • 133
  • 218
  • 1
    Unfortunately, the type `T` is no longer particularly informative. –  Sep 04 '17 at 12:16
  • @ftor What kind of information do you want to preserve? What kind of type would you expect? – chi Sep 04 '17 at 12:57
  • I just meant that with hiding the recursive type the type annotation is no longer particularly useful to conclude the space of possible computations from it - at least in this very case. You could have chosen a more meaningful name for the newtype, but still would exchange a type signature with a simple name. –  Sep 04 '17 at 14:11
  • @ftor I see. Below leftaroundabout provides a more informative type expression like `Fix (ListT ((->) Int))`. In the general case, we would need type-level functions, like `Fix (\T -> (Int -> [T]))` but these are not supported by Haskell. – chi Sep 04 '17 at 14:25
3

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'
leftaroundabout
  • 117,950
  • 5
  • 174
  • 319
  • `fix` is indeed intriguing. This is a good opportunity for me to get a better idea of the concept. Thanks! –  Sep 04 '17 at 14:19