代码之家 › 专栏 › 技术社区 › Asad Saeeduddin

定义arity通用提升

type-families applicative dependent-type haskell

1

Asad Saeeduddin · 技术社区 · 7 年前

我在试着定义 liftN 哈斯克尔。动态类型语言(如JS)中的值级实现相当简单,我在用Haskell表达它时遇到了困难。

经过一些尝试和错误之后,我得出了下面的类型检查(请注意 升降机 是 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 到(最后),实际的递归实现 升降机 。

不幸的是我连 纯净的 和 地图 要进行类型检查的案例。以下是我添加的内容(注意 go 仍然是 未定义 ):

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.

在这一点上,我不清楚究竟是什么模棱两可或如何消除它的歧义。

是否有一种方法可以优雅地(或者如果不是如此优雅地,以一种将不雅限制到功能实现的方式)实现 升降机 在这里?

1 回复 | 直到 7 年前

1

3

oisdk 7 年前

这里有两个问题:

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

此示例改编自 Richard Eisenberg's thesis .