Воссоздание Lisp `apply` в Haskell с использованием GADT

Question

В качестве упражнения я пытаюсь воссоздать Лисп apply в Хаскеле. Я не собираюсь использовать это для каких-либо практических целей, я просто думаю, что это хорошая возможность познакомиться с системой типов Хаскелла и системами типов в целом. (Так что я также не ищу реализации других людей.)

Моя идея заключается в следующем: я могу использовать GADT, чтобы "пометить" список типом функции, к которой он может быть применен. Итак, я переопределяю Nil а также Cons таким же образом, что мы закодировали бы длину списка в типе, используя Nat определение, но вместо использования чисел Пеано длина определенным образом кодируется в типе функции тегирования (т. е. длина соответствует числу аргументов функции).

Вот код, который у меня есть:

{-# LANGUAGE GADTs #-}

-- n represents structure of the function I apply to
-- o represents output type of the function
-- a represents argument type of the function (all arguments same type)
data FList n o a where
  -- with Nil the function is the output
  Nil :: FList o o a
  -- with Cons the corresponding function takes one more argument
  Cons :: a -> FList f o a -> FList (a -> f) o a

args0 = Nil :: FList Int Int Int -- will not apply an argument
args1 = Cons 1 args0 -- :: FList (Int -> Int) Int Int
args2 = Cons 2 args1 -- :: FList (Int -> Int -> Int) Int Int
args3 = Cons 3 args2 -- :: FList (Int -> Int -> Int -> Int) Int Int

listApply :: (n -> o) -> FList (n -> o) o a -> o
-- I match on (Cons p Nil) because I always want fun to be a function (n -> o)
listApply fun (Cons p Nil) = fun p
listApply fun (Cons p l) = listApply (fun p) l

main = print $ listApply (+) args2

В последней строке моя идея будет (+) будет иметь тип Int -> Int -> Int, где Int -> Int соответствует n в (n -> o) а также o соответствует последнему Int (вывод) [1]. Насколько я могу судить, этот тип, кажется, работает с типом моего argsN определения.

Тем не менее, я получаю две ошибки, из которых я укажу компонент, который мне кажется актуальным:

test.hs:19:43:
    Could not deduce (f ~ (n0 -> f))
    from the context ((n -> o) ~ (a -> f))
      bound by a pattern with constructor
                 Cons :: forall o a f. a -> FList f o a -> FList (a -> f) o a,
               in an equation for ‘listApply’

а также

test.hs:21:34:
    Couldn't match type ‘Int’ with ‘Int -> Int’
    Expected type: FList (Int -> Int -> Int) (Int -> Int) Int
      Actual type: FList (Int -> Int -> Int) Int Int
    In the second argument of ‘listApply’, namely ‘args2’

Я не уверен, как интерпретировать первую ошибку. Вторая ошибка сбивает меня с толку, поскольку она не совпадает с моей интерпретацией, отмеченной ранее [1].

Любое понимание того, что происходит не так?

PS: я более чем готов узнать о новых расширениях, если это поможет.

Answer 1

Вы поняли это почти правильно. Рекурсия должна соответствовать структуре GADT:

{-# LANGUAGE GADTs #-}
-- n represents structure of the function I apply to
-- o represents output type of the function
-- a represents argument type of the function (all arguments same type)
data FList n o a where
  -- with Nil the function is the output
  Nil :: FList o o a
  -- with Cons the corresponding function takes one more argument
  Cons :: a -> FList f o a -> FList (a -> f) o a

args0 = Nil :: FList Int Int Int -- will not apply an argument
args1 = Cons 1 args0 -- :: FList (Int -> Int) Int Int
args2 = Cons 2 args1 -- :: FList (Int -> Int -> Int) Int Int
args3 = Cons 3 args2 -- :: FList (Int -> Int -> Int -> Int) Int Int

-- n, not (n -> o)
listApply :: n -> FList n o a -> o
listApply fun Nil = fun
listApply fun (Cons p l) = listApply (fun p) l

main = print $ listApply (+) args2

three :: Int
three = listApply (+) (Cons 2 (Cons 1  Nil))

oof :: String
oof = listApply reverse (Cons "foo" Nil)

true :: Bool
true = listApply True Nil -- True

-- The return type can be different than the arguments:

showplus :: Int -> Int -> String
showplus x y = show (x + y)

zero :: String
zero = listApply showplus (Cons 2 (Cons 1 Nil))

---

Надо сказать, что это выглядит довольно элегантно!

---

Даже ОП не требует реализации других людей. Вы можете подойти к проблеме немного по-другому, что приведет к другому, но аккуратному API:

{-# LANGUAGE KindSignatures #-}
{-# LANGuAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Proxy

data N = O | S N

p0 :: Proxy O
p1 :: Proxy (S O)
p2 :: Proxy (S (S O))
p0 = Proxy
p1 = Proxy
p2 = Proxy

type family ArityNFun (n :: N) (a :: *) (b :: *) where
  ArityNFun O a b = b
  ArityNFun (S n) a b = a -> ArityNFun n a b

listApply :: Proxy n -> ArityNFun n a b -> ArityNFun n a b
listApply _ = id

three :: Int
three = listApply p2 (+) 2 1

oof :: String
oof = listApply p1 reverse "foo"

true :: Bool
true = listApply p0 True

showplus :: Int -> Int -> String
showplus x y = show (x + y)

zero :: String
zero = listApply p2 showplus 0 0

Здесь мы могли бы использовать Nat от GHC.TypeLits, но тогда нам нужно UndecidableInstances, Добавленный сахар не стоит хлопот в этом примере.

Если вы хотите сделать полиморфную версию, это тоже возможно, но тогда индекс не (n :: Nat) (a :: *) но (as :: [*]), Также делает plusN может быть хорошим упражнением для обеих кодировок.

Answer 2

Не то же самое, но я подозреваю, что вас заинтересует бесплатный аппликативный функтор, который free библиотека предоставляет. Это происходит примерно так (в зависимости от реализации в free, но используя :<**> конструктор вместо Ap):

data Ap f a where
  Pure :: a -> Ap f a
  (:<**>) :: f x -> Ap f (x -> a) -> Ap f a

Вы можете думать о них как о неоднородно типизированном списке с элементами типов f x0,..., f xn, прекращено Pure (f :: x0 -> ... -> xn -> a), Это похоже на "синтаксическое дерево" для аппликативных вычислений, позволяющее вам использовать обычные аппликативные методы для построения "дерева", которое может отдельно запускаться функциями интерпретатора.

---

Упражнение: реализовать следующие примеры:

instance Functor f => Functor (Ap f) where ...
instance Functor f => Applicative (Ap f) where ...

Подсказка: Applicative законы предоставляют рецепт, который вы можете использовать для их реализации.