Type families - cannot derive Base Int?

Question

The idea is to implement "lazy" length function to compare list length to a Int without computing the whole length.

{-# LANGUAGE DeriveFunctor
           , TypeFamilies
           , FlexibleInstances #-}
import Data.Functor.Foldable

type instance Base Int   = Maybe

Now we can have Foldable / Unfoldable

instance Foldable Int where
  project 0 = Nothing
  project x = Just (x-1)

instance Unfoldable Int where
  embed Nothing  = 0
  embed (Just x) = x+1

I want to convert [a] into Base Int Int:

leng :: [a] -> Base Int Int
leng = ana phi where
  phi :: [a] -> Base Int [a]
  phi []    = Nothing
  phi (_:t) = Just t

But this doesn't work. It complains [a] -> Base (Maybe Int) [a] is expected as type of phi. I don't understand why.

If that worked, then I can compare:

gt = curry $ hylo psi phi where
  phi (Just _, Nothing)  = Left True
  phi (Nothing, _)       = Left False
  phi (Just t, Just n)   = Right (t, n)

  psi (Left t)  = t
  psi (Right t) = t

main = print $ (leng [1..]) `gt` (ana project 4)

What's wrong with leng?

Answer 1

The type of ana is (a -> Base t a) -> a -> t. Note that it returns the plain t and not Base t t. So the correct type for leng is

leng :: [a] -> Int

Answer 2

Thanks for pointing out the type is wrong. Getting the type right clarified the thought :)

{-# LANGUAGE DeriveFunctor
           , TypeFamilies
           , FlexibleInstances #-}
import Data.Functor.Foldable

type instance Base ([a], Int) = Either Bool

instance Foldable ([a], Int) where
  project ([], _) = Left False
  project (_, 0) = Left True
  project ((h:t), n) = Right (t, n-1)

longerThan :: [a] -> Int -> Bool
longerThan = curry $ cata $ either id id

main = print $ [1..] `longerThan` 4

Satisfied? Let's extend this to show why I really started all this:

{-# LANGUAGE DeriveFunctor
           , TypeFamilies
           , FlexibleInstances
           , FlexibleContexts
           , UndecidableInstances #-}
import Data.Functor.Foldable

data Zip a b x = Z (Base a (Base b x))
instance (Functor (Base a), Functor (Base b)) => Functor (Zip a b) where
  fmap f (Z a) = Z $ fmap (\x -> fmap f x) a

type instance Base (a, b) = Zip a b

Get the hint? We can recurse both structures at the same time!

instance (Foldable a, Foldable b) => Foldable (a, b) where
  project (a, b) = Z $ fmap (\x -> fmap (\y -> (x,y)) $ project b) $ project a

Demo: introduce Base Int, and check the length of the list is greater than a given Int.

type instance Base Int = Maybe

instance Foldable Int where
  project 0 = Nothing
  project x = Just $ x-1

-- lt and gt are the same;
-- just showing off with the order of arguments, so you can appreciate Zip
lt :: Int -> [a] -> Bool
lt = curry $ cata phi where
  phi (Z Nothing) = True
  phi (Z (Just Nil)) = False
  phi (Z (Just (Cons _ t))) = t

gt :: [a] -> Int -> Bool
gt = curry $ cata phi where
  phi (Z (Cons _ Nothing)) = True
  phi (Z Nil) = False
  phi (Z (Cons _ (Just t))) = t

main = print [[1..] `gt` 4, 4 `lt` [1..]]

Answer 3

This may defeat the purpose of the exercise of doing it with type families, but if you simply want a 'lazily compare list length with int'-function you can just write it directly:

cmp :: [a] -> Int -> Ordering
cmp [] n = compare 0 n
cmp (_:xs) n = if n <= 0 then GT else cmp xs (n - 1)

Answer 4

The same function that @PaulVisschers is implementing, which is indeed one of the simplest ways to do what you want, can be implemented with a catamorphism, if for some reason you want an exercise with Foldables.

import Data.Functor.Foldable

cmp :: [a] -> Int -> Ordering
cmp = cata psi

psi :: Base [a] (Int -> Ordering) -> Int -> Ordering
psi Nil n = compare 0 n
psi (Cons h t) n = if n <= 0 then GT else t (n-1)