Is posible to create an infinite wrapper in Haskell with Rank N types?

Question

I tried this experiment:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}

wrapper :: forall a (b :: * -> *). Monad b => Int -> a -> b a
wrapper 1 v = return v
wrapper n v = return $ wrapper (n-1) v

But it gives to me the error:

 Occurs check: cannot construct the infinite type: a ~ b0 a
      Expected type: b a
        Actual type: b (b0 a)
    • In the expression: return $ wrapper (n - 1) v
      In an equation for ‘wrapper’:
          wrapper n v = return $ wrapper (n - 1) v
    • Relevant bindings include
        v :: a (bound at main.hs:7:11)
        wrapper :: Int -> a -> b a (bound at main.hs:6:1)

Is it possible to create the function wrapper such as:

wrapper 4 'a' :: [Char]
[[[['a']]]]

Infinite types are not possible in any situation. You'd have to hide this complexity behind a constructor. However, this would just be the same as an infinite list e.g. foo = () : foo. Related question: stackoverflow.com/questions/9566683/… — AJF

oisdk oisdk · Accepted Answer · 2019-08-15T22:33:58

Yes and no!

First of all, your type is inaccurate in the signature of the function. Taking your example of wrapper 4 'a', the return type of the function is m (m (m (m a))) (where m is []), not m a.

Secondly, we're not allowed infinite types in Haskell's type system, so we wouldn't be able to write down the correct type even if we wanted to!

That said, we can address both of these concerns with some new types that will do the type-level recursion for us. First, there's Fix:

newtype Fix f a = Fix { unFix :: f (Fix f a) }

Using this we can wrap infinitely:

wrap :: Monad m => Fix m a
wrap = Fix $ return $ wrap

As you can see, we don't need the base element (the a in your example) because we'll never hit the base of the recursion.

But that's not what you wanted either! The "infinite" here is actually something of a red herring: you want to be able to wrap something a finite number of times, using an argument to dictate the wrapping level.

You can do something like this with another wrapper:

data Wrap f a = Pure a | Wrap (f (Wrap f a))

wrapper :: Monad f => Int -> a -> Wrap f a
wrapper 0 x = Pure x
wrapper n x = Wrap $ pure $ wrapper (n-1) x

(This is in fact the free monad that we're using here)

What you're looking for exactly, though (i.e., no wrappers) can be done, however, it's quite involved, and probably not what you're looking for. I'll include it for completeness nonetheless.

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE TypeApplications     #-}

import Data.Kind
import GHC.TypeLits

data N = Z | S N

type family Wrap (n :: N) (f :: Type -> Type) (a :: Type) :: Type where
  Wrap Z f a = a
  Wrap (S n) f a = Wrap n f (f a)

type family FromNat (n :: Nat) :: N where
  FromNat 0 = Z
  FromNat n = S (FromNat (n - 1))

data Ny (n :: N) where
  Zy :: Ny Z
  Sy :: Ny n -> Ny (S n)

class KnownN n where sing :: Ny n
instance KnownN Z where sing = Zy
instance KnownN n => KnownN (S n) where sing = Sy sing

wrap :: forall n f a. (KnownN (FromNat n), Monad f) => a -> Wrap (FromNat n) f a
wrap = go @(FromNat n) @f @a sing
  where
    go :: forall n f a. Monad f => Ny n -> a -> Wrap n f a
    go Zy x = x
    go (Sy n) x = go @_ @f n (return @f x)


main = print (wrap @4 'a' == [[[['a']]]])

Is posible to create an infinite wrapper in Haskell with Rank N types?

1 Answers