Skip to content

Instantly share code, notes, and snippets.

@plaidfinch
Created October 27, 2014 20:51
Show Gist options
  • Save plaidfinch/95ca8b2b8ac859ab25f3 to your computer and use it in GitHub Desktop.
Save plaidfinch/95ca8b2b8ac859ab25f3 to your computer and use it in GitHub Desktop.
{-# 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment