PolymorphicFixedpoints.hs

{-# LANGUAGE DataKinds  #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs      #-}
{-# LANGUAGE PolyKinds  #-}

-- How to use fix to implement polymorphic recursion!

module PolymorphicFixedpoints where

import Data.Function ( fix )
-- This is all we need from there:
-- fix :: (a -> a) -> a
-- fix f = let x = f x in x

-- A Cocone from f to r is a function (∀ a. f a -> r).
-- Taken from the (deprecated) category-extras package;
-- specifically, from Data.Functor.Cone.
newtype Cocone (f :: k -> *) (r :: *) =
   Cocone { runCocone :: forall a. f a -> r }

-- Defining singleton natural numbers using DataKinds...
data N = Z | S N
data Nat (n :: N) where
   Zero :: Nat Z
   Succ :: Nat n -> Nat (S n)

-- A non-recursive function which takes a (∀ n. Nat n -> Integer) and returns one.
-- It is the single (polymorphic) inductive step we need for our recursive function.
countWith :: Cocone Nat Integer -> Cocone Nat Integer
countWith f = Cocone $
   \n -> case n of
      Zero   -> 0
      Succ x -> 1 + runCocone f x

-- A polymorphically recursive function (∀ n. Nat n -> Integer), which translates
-- from singleton naturals to normal integers. Note that the only recursion in this
-- entire file is in the definition of fix.
count :: Nat n -> Integer
count = runCocone $ fix countWith

-- Why all this silliness with the Cocone newtype?
-- You might think that the following approach would work ...

countWith' :: (forall a. Nat a -> Integer) -> (forall b. Nat b -> Integer)
countWith' f =
   \n -> case n of
      Zero   -> 0
      Succ x -> 1 + f x

-- ... but it doesn't, because the following won't type-check:

--count' :: Nat n -> Integer
--count' = fix countWith'

-- GHC says: Couldn't match type ‘forall (a :: N). Nat a -> Integer’ with ‘Nat n -> Integer’
--
-- This is because it floats the second universal quantification to the beginning
-- of the signature for countWith, so that it reads:
--
-- > forall b. (forall a. Nat a -> Integer) -> Nat b -> Integer
--
-- But now, when we go to take its fixed point using (fix :: forall a. (a -> a) -> a),
-- there's no way to instantiate the `a' type variable for fix, as the *actual* form
-- of countWith' (as GHC finally interprets it) is not of the form (a -> a). In order to
-- prevent this ∀-floating, we need to wrap things in a newtype, which is the approach
-- I demonstrate above by means of Cocone.