Определение арности-общего лифта - PullRequest
Новая
       84

Определение арности-общего лифта

0 голосов
/ 29 мая 2018

Я пытаюсь определить liftN для Haskell.Реализация на уровне значений в динамически типизированных языках, таких как JS, довольно проста, у меня просто возникают проблемы с ее выражением в Haskell.

После некоторых проб и ошибок я пришел к следующему: какие проверки типов (обратите внимание на весьреализация liftN is undefined): 

{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}

import Data.Proxy
import GHC.TypeLits

type family Fn x (y :: [*]) where
  Fn x '[]    = x
  Fn x (y:ys) = x -> Fn y ys

type family Map (f :: * -> *) (x :: [*]) where
  Map f '[]     = '[]
  Map f (x:xs)  = (f x):(Map f xs)

type family LiftN (f :: * -> *) (x :: [*]) where
  LiftN f (x:xs)  = (Fn x xs) -> (Fn (f x) (Map f xs))

liftN :: Proxy x -> LiftN f x
liftN = undefined

Это дает мне желаемое поведение в ghci: 

*Main> :t liftN (Proxy :: Proxy '[a])
liftN (Proxy :: Proxy '[a]) :: a -> f a

*Main> :t liftN (Proxy :: Proxy '[a, b])
liftN (Proxy :: Proxy '[a, b]) :: (a -> b) -> f a -> f b

и т. д.

ЧастьЯ озадачен тем, как на самом деле это реализовать.Я подумал, что, возможно, самый простой способ - обменять список уровней типа на номер уровня типа, представляющий его длину, использовать natVal, чтобы получить соответствующий номер уровня значения, а затем отправить 1 в pure, 2 вmap и n до (наконец) фактической рекурсивной реализации liftN.

К сожалению, я не могу даже проверить случаи pure и map.Вот что я добавил (примечание go по-прежнему undefined): 

type family Length (x :: [*]) where
  Length '[]    = 0
  Length (x:xs) = 1 + (Length xs)

liftN :: (KnownNat (Length x)) => Proxy x -> LiftN f x
liftN (Proxy :: Proxy x) = go (natVal (Proxy :: Proxy (Length x))) where
  go = undefined

Пока все хорошо.Но тогда: 

liftN :: (Applicative f, KnownNat (Length x)) => Proxy x -> LiftN f x
liftN (Proxy :: Proxy x) = go (natVal (Proxy :: Proxy (Length x))) where
  go 1 = pure
  go 2 = fmap
  go n = undefined

... беда наносит удар: 

Prelude> :l liftn.hs
[1 of 1] Compiling Main             ( liftn.hs, interpreted )

liftn.hs:22:28: error:
    * Couldn't match expected type `LiftN f x'
                  with actual type `(a0 -> b0) -> (a0 -> a0) -> a0 -> b0'
      The type variables `a0', `b0' are ambiguous
    * In the expression: go (natVal (Proxy :: Proxy (Length x)))
      In an equation for `liftN':
          liftN (Proxy :: Proxy x)
            = go (natVal (Proxy :: Proxy (Length x)))
            where
                go 1 = pure
                go 2 = fmap
                go n = undefined
    * Relevant bindings include
        liftN :: Proxy x -> LiftN f x (bound at liftn.hs:22:1)
   |
22 | liftN (Proxy :: Proxy x) = go (natVal (Proxy :: Proxy (Length x))) where
   |                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

На данный момент мне не ясно, что именно является двусмысленным или как устранить неоднозначность.

Есть ли способ элегантно (или, если не так элегантно, так, чтобы неравенство ограничивалось реализацией функции) реализовать здесь тело liftN?

1 Ответ

0 голосов
/ 29 мая 2018

Здесь есть две проблемы:

  • Вам нужно больше, чем просто natVal числа уровня типа, чтобы обеспечить проверку всех типов функций: вам также нужно доказательство того, что структураВы повторяете, соответствует номеру уровня типа, на который вы ссылаетесь.Integer сам по себе теряет всю информацию об уровне типа.
  • И наоборот, вам нужно больше информации времени выполнения, чем просто типа: в Haskell типы не имеют представления времени выполнения, поэтому передача Proxy aтак же, как проходящий в ().Вам нужно получить информацию о времени выполнения где-нибудь.

Обе эти проблемы можно решить с помощью синглетонов или классов: 

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}

data Nat = Z | S Nat

type family AppFunc f (n :: Nat) arrows where
  AppFunc f Z a = f a
  AppFunc f (S n) (a -> b) = f a -> AppFunc f n b

type family CountArgs f where
  CountArgs (a -> b) = S (CountArgs b)
  CountArgs result = Z

class (CountArgs a ~ n) => Applyable a n where
  apply :: Applicative f => f a -> AppFunc f (CountArgs a) a

instance (CountArgs a ~ Z) => Applyable a Z where
  apply = id
  {-# INLINE apply #-}

instance Applyable b n => Applyable (a -> b) (S n) where
  apply f x = apply (f <*> x)
  {-# INLINE apply #-}

-- | >>> lift (\x y z -> x ++ y ++ z) (Just "a") (Just "b") (Just "c")
-- Just "abc"
lift :: (Applyable a n, Applicative f) => (b -> a) -> (f b -> AppFunc f n a)
lift f x = apply (fmap f x)
{-# INLINE lift #-}

Этот пример адаптирован из РичардТезис Эйзенберга .

...