Можно ли повторить применение неэндоморфизма? - PullRequest
Новая
       33

Можно ли повторить применение неэндоморфизма?

0 голосов
/ 11 июня 2018

В Haskell, если я хочу многократно применять эндоморфизм a -> a к значению типа a, я могу просто использовать iterate.

Как насчет функции, которая не является эндоморфизмом, но является общейдостаточно для корректной работы с типом возвращаемого значения?

Рассмотрим, например, Just :: a -> Maybe a;Я могу написать 

Just . Just . Just ...

столько раз, сколько захочу.Есть ли способ написать это в ближайшее время с помощью что-то вроде 

iterate' 3 Just :: a -> Maybe (Maybe (Maybe a))

или нам нужно что-то вроде зависимых типов для этого?

Ответы [ 2 ]

0 голосов
/ 12 июня 2018

Это возможно с незначительной настройкой предложенного вами синтаксиса: iterate' @3 Just вместо iterate' 3 Just.

Это потому, что тип результата зависит от числа, поэтому число должно быть тип литерал , а не значение литерал .Как вы правильно заметили, для выполнения этого с произвольными числами потребуются зависимые типы [1], которых у Haskell нет. 

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies, KindSignatures, DataKinds,
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables,
    FunctionalDependencies, TypeApplications, RankNTypes, FlexibleContexts,
    AllowAmbiguousTypes #-}

import qualified GHC.TypeLits as Lit

-- from type-natural
import Data.Type.Natural
import Data.Type.Natural.Builtin

class Iterate (n :: Nat) (f :: * -> *) (a :: *) (r :: *)
  | n f a -> r
  where
  iterate_peano :: Sing n -> (forall b . b -> f b) -> a -> r

instance Iterate 'Z f a a where
  iterate_peano SZ _ = id
instance Iterate n f (f a) r => Iterate ('S n) f a r where
  iterate_peano (SS n) f x = iterate_peano n f (f x)

iterate'
  :: forall (n :: Lit.Nat) f a r .
     (Iterate (ToPeano n) f a r, SingI n)
  => (forall b . b -> f b) -> a -> r
iterate' f a = iterate_peano (sToPeano (sing :: Sing n)) f a

Если вы загрузите это в ghci, вы можете сказать 

*Main> :t iterate' @3 Just
iterate' @3 Just :: a -> Maybe (Maybe (Maybe a))
*Main> iterate' @3 Just True
Just (Just (Just True))

В этом коде используются два натуральных числа уровня типа: встроенные Nat из GHC.TypeLits и классические цифры Пеано из Data.Type.Natural.Первые необходимы для обеспечения хорошего синтаксиса iterate' @3, вторые необходимы для выполнения рекурсии (что происходит в классе Iterate).Я использовал Data.Type.Natural.Builtin для преобразования из литерала в соответствующую цифру Пеано.

[1] Однако, учитывая конкретный способ использования повторяющихся значений (например, если вы заранее знаете, что вам нужно толькоshow их), вы, вероятно, могли бы адаптировать этот код для работы даже для динамических значений n.В типе iterate' нет ничего, что требовало бы статически известного Nat;единственная задача состоит в том, чтобы доказать, что результат итерации удовлетворяет необходимым ограничениям.

0 голосов
/ 11 июня 2018

Вы можете сделать это с шаблоном haskell, если вы знаете число во время компиляции (но, если число не очень большое, я не думаю, что это стоит хлопот).Если вы еще не знаете номер во время компиляции, вам нужно правильно смоделировать тип возвращаемого значения, что мы можем сделать, используя нерегулярный тип: 

data Iter f a = Iter0 a | IterS (Iter f (f a))

iterate' :: Int -> (forall x. x -> f x) -> a -> Iter f a
iterate' 0 f x = Iter0 x
iterate' n f x = IterS (iterate' (n-1) f (f x))

Iter по сути является способомвыражая тип данных a | f a | f (f a) | f (f (f a)) | ....Для использования результата вам необходимо набрать сумму Iter.Кроме того, функция должна иметь форму a -> f a для какого-либо конструктора типа f, поэтому вам может потребоваться выполнить обтекание нового типа, чтобы туда попасть.Так что ... в любом случае это какая-то боль.

...