Можно ли создать бесконечную оболочку в Haskell с типами ранга N?

Я попробовал этот эксперимент:

{-# 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

Но это дает мне ошибку:

 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)

Можно ли создать оболочку функции, например:

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

haskell rank-n-types
person Damián Rafael Lattenero    schedule 15.08.2019    source источник
comment
Бесконечные типы невозможны ни в какой ситуации. Вам придется скрыть эту сложность за конструктором. Однако это будет то же самое, что и бесконечный список, например. foo = () : foo. Связанный вопрос: stackoverflow.com/questions/9566683 /   -  person AJF    schedule 16.08.2019

Ответы (1)


arrow_upward
4
arrow_downward

И да и нет!

Прежде всего, ваш тип неточен в подписи функции. Взяв ваш пример wrapper 4 'a', возвращаемый тип функции — m (m (m (m a))) (где m — это []), а не m a.

Во-вторых, нам не разрешены бесконечные типы в системе типов Haskell, поэтому мы не сможем записать правильный тип, даже если захотим!

Тем не менее, мы можем решить обе эти проблемы с помощью некоторых новых типов, которые будут выполнять за нас рекурсию на уровне типов. Во-первых, Fix:

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

Используя это, мы можем обертывать бесконечно:

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

Как видите, нам не нужен базовый элемент (в вашем примере a), потому что мы никогда не попадем в базу рекурсии.

Но это не то, что вы хотели! «Бесконечность» здесь на самом деле является чем-то вроде отвлекающего маневра: вы хотите иметь возможность оборачивать что-то конечное число раз, используя аргумент, определяющий уровень обтекания.

Вы можете сделать что-то подобное этому с другой оболочкой:

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

(На самом деле это свободная монада, которую мы здесь используем)

То, что вы ищете, именно, хотя (т. е. без оберток) можно сделать, однако это довольно сложно и, вероятно, не то, что вы ищете. Тем не менее, я включу его для полноты.

{-# 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']]]])
person oisdk    schedule 15.08.2019