Я пытаюсь определить 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
?