unfold-foldl.hs

-- Compile with
-- ghc -Wall -O -fforce-recomp -ddump-simpl -dsuppress-all poly.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Poly (value, ualue, xalue) where

import Data.Proxy (Proxy (..))

data N = Z | S N
type N5 = 'S ('S ('S ('S ('S 'Z))))
type N7 = 'S ('S N5)

type Bound = N5

-- Dictionary inlines better if it's single value. ¯\_(ツ)_/¯
class Foldl (n :: N) where
    left  :: proxy n -> (b -> a -> b) -> b -> [a] -> b

instance Foldl 'Z where
    left _ f z = go z where
        go !acc []       = acc
        go !acc (x : xs) = go (f acc x) xs

instance Foldl n => Foldl ('S n) where
    left _ _ z []       = z
    left _ f z (x : xs) = left (Proxy :: Proxy n) f (f z x) xs

foldl' :: forall a b. (b -> a -> b) -> b -> [a] -> b
foldl' = left (Proxy :: Proxy Bound)

-- | Core:
--
-- @
-- -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-- value
-- value = I# 10#
-- @
--
value :: Int
value = foldl' (+) 0 [1,2,3,4]

-- This doesn't work out because 'enumFromTo' is recursive :(
ualue :: Int
ualue = foldl' (+) 0 [1..100]

-------------------------------------------------------------------------------
-- Second try
-------------------------------------------------------------------------------

class Unfoldr (n :: N) where
    unf :: proxy n -> (b -> Maybe (a, b)) -> b -> [a]

instance Unfoldr 'Z where
    unf _ f = go where
        go z = case f z of
            Nothing     -> []
            Just (a, b) -> a : go b
        

instance Unfoldr n => Unfoldr ('S n) where
    unf _ f z = case f z of
        Nothing     -> []
        Just (a, b) -> a : unf (Proxy :: Proxy n) f b

unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
unfoldr = unf (Proxy :: Proxy Bound)

-- | Core;
--
-- @
-- -- RHS size: {terms: 8, types: 1, coercions: 0, joins: 0/0}
-- xalue
-- xalue
--  = case $wgo2 15# ($wgo1 6#) of ww_s2ZA { __DEFAULT -> I# ww_s2ZA }
--
-- Rec {
-- -- RHS size: {terms: 22, types: 7, coercions: 0, joins: 0/0}
-- $wgo1
-- $wgo1
--   = \ ww_s2Zo ->
--       case tagToEnum# (># ww_s2Zo 100#) of {
--         False ->
--           : (I# ww_s2Zo)
--             (case ww_s2Zo of wild1_a2Ny {
--                __DEFAULT -> $wgo1 (+# wild1_a2Ny 1#);
--                9223372036854775807# -> case $fEnumInt2 of wild2_00 { }
--              });
--         True -> []
--       }
-- end Rec }
--
-- Rec {
-- -- RHS size: {terms: 15, types: 10, coercions: 0, joins: 0/0}
-- $wgo2
-- $wgo2
--   = \ ww_s2Zf w_s2Zc ->
--       case w_s2Zc of {
--         [] -> ww_s2Zf;
--         : x_aXn xs_aXo ->
--           case x_aXn of { I# y_X2NU -> $wgo2 (+# ww_s2Zf y_X2NU) xs_aXo }
--       }
-- end Rec }
-- @

xalue :: Int
xalue = foldl' (+) 0 (myEnumFromTo 1 100)

myEnumFromTo :: Enum a => a -> a -> [a]
myEnumFromTo x y = unfoldr f (fromEnum x) where
    y' = fromEnum y
    f z | z > y'     = Nothing
        | otherwise = Just (toEnum z, succ z)

-------------------------------------------------------------------------------
-- Bonus
-------------------------------------------------------------------------------

class Foldr (n :: N) where
    right :: proxy n -> (a -> b -> b) -> b -> [a] -> b 

instance Foldr 'Z where
    right _ f z = go where
        go [] = z
        go (x : xs) = f x (go xs)

instance Foldr n => Foldr ('S n) where
    right _ _ z []       = z
    right _ f z (x : xs) = f x (right (Proxy :: Proxy n) f z xs)

xalue reduces statically to 5050 if you make the bound big enough. 5 is certainly not enough to unroll a list of 100 elements.

@kosmikus: as told face-2-face, the xvalue shows that GHC unrolls 5 first steps (starts with 16): it does exactly as much unrolling as I expect.

Trying to get it : the first example shows that if we know the list is at least of some size n, we can unroll statically the n recursive calls from the base case. instead of having foldl z s xs we (statically) rewrite it, say, foldl (s (s (s z x1) x2) x3) s xs, so the optimizer will inline the s calls and compute the first value statically.

It the case of a structure coming from an unfold (like [1..100] ), this fails as it is defined recursively at value level. We do the same process of inlining as much as is known at type level, replacing unfoldr f x by x:(s x):(s (s x)):unfoldr (s (s (x))).

The compiler can now optimize the overall computation in xvalue.
The information was thrown away in the result type of myEnumFromTo, but it does not prevent the simplification to happen.

Is it a correct reading of what is going on ? (ps : Interesting example, thank you for sharing it)

@nrolland yes, you read it exactly right. (Gists don't give me notifications, sorry for very late response)