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

Question

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

Моя идея следующая: я могу использовать 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].

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

P.S: Я более чем готов узнать о новых расширениях, если это сделает эту работу.

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 applicative functor, который предоставляет free library. Это идет что-то вроде этого (на основе реализации в 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 законы обеспечивают рецепт, который вы можете использовать для реализации этих.