使用GADT在Haskell中重新创建Lisp的`apply' [英] Recreating Lisp's `apply` in Haskell using GADTs
问题描述
apply 。我不打算将此用于任何实际目的，我只是认为这是一个很好的机会，可以更全面地熟悉Haskell的类型系统和类型系统。 （所以我也没有在寻找其他人的实现。） 我的想法如下：我可以使用GADT来用功能类型标记列表它可以应用于。因此，我重新定义了 Nil 和 Cons ，类似于我们使用 Nat 定义，但不是使用Peano数字，而是使用标记函数类型编码长度（即长度对应于函数参数的数量）。
下面是我到目前为止的代码：
{ - ＃LANGUAGE GADTs＃ - }
- n表示函数的结构我应用于
- o表示函数的输出类型
- a表示函数的参数类型（所有参数相同类型）
数据FList noa其中
- 无无函数是输出
无:: FList ooa
- 带缺省值的相应函数需要多一个参数
缺点：a - > FList f o a - > FList（a - > f）oa
args0 = Nil :: FList Int Int Int - 不会应用参数
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
- 我匹配（Cons p Nil），因为我总是希望有趣的是一个函数（n - > o）
listApply fun（Cons p Nil）= fun p
listApply fun（Cons pl）= listApply（fun p）l
main = print $ listApply（+）args2
在最后一行中，我的想法是（+）的类型是 Int - > Int - > Int ，其中 Int - > Int 对应于（n - > o）和<$ c中的 n $ c> o 对应于最后一个 Int （输出）[1]。据我所知，这种类型似乎解决了我的 argsN 定义的类型。
然而， ，我得到两个错误，其中我将陈述与我相关的组件：
test.hs：19：43 ：
无法从上下文（（n - > o）〜（a - > f））
中推导出（f〜（n0 - > f））
模式与构造函数
Cons :: forall oa f。 a - > FList f o a - >在'listApply'
等式中，FList（a - > f）oa，
。和
test.hs：21：34：
无法将类型'Int'与'Int - > ; Int'
预期类型：FList（Int - > Int - > Int）（Int - > Int）Int
实际类型：FList（Int - > Int - > Int）Int Int
在'listApply'的第二个参数中，即'args2'
我不是确定如何解释第一个错误。第二个错误让我感到困惑，因为它与我前面标注[1]的解释不符。
任何洞察哪里出错？
PS：我非常乐意学习新的扩展功能，如果这样做能够实现这一功能的话。 h2_lin>解决方案
你明白了。递归应遵循GADT的结构：
{ - ＃LANGUAGE GADTs＃ - }
- n表示结构函数I适用于
- o表示函数的输出类型
- a表示函数的参数类型（所有参数相同类型）
数据FList noa其中
- - 无Nil函数是输出
Nil :: FList ooa
- 与缺省值相对应的函数需要多一个参数
缺陷:: a - > FList f o a - > FList（a - > f）oa
args0 = Nil :: FList Int Int Int - 不会应用参数
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 pl）= listApply（fun p）l
main = print $ listApply（+）args2
three :: Int
three = listApply（+）（Cons 2（Cons 1 Nil））
oof :: String
oof = listApply reverse（Consfoo无）
true :: Bool
true = listApply True无 - True
- 返回类型可以与参数不同：
showplus :: Int - > Int - > String
showplus xy = show（x + y）
zero :: String
zero = listApply showplus（Cons 2（Cons 1 Nil））
必须说，这看起来相当优雅！
即使OP不要求其他人的实现。你可以用不同的方式来处理问题，从而得到一个不同但看起来整齐的API：
{ - ＃LANGUAGE KindSignatures＃ - }
{ - ＃LANGuAGE DataKinds＃ - }
{ - ＃LANGUAGE PolyKinds＃ - }
{ - ＃LANGUAGE TypeFamilies＃ - }
{ - ＃LANGUAGE TypeOperators＃ - }
{ - ＃LANGUAGE AllowAmbiguousTypes＃ - }
导入Data.Proxy
数据N = O | SN
p0 ::代理O
p1 ::代理（SO）
p2 ::代理（S（SO））
p0 =代理
p1 =代理
p2 =代理
类型系列ArityNFun（n :: N）（a :: *）（b :: *）其中
ArityNFun O ab = b
ArityNFun（S n）ab = a - > ArityNFun n a b
listApply :: Proxy n - > ArityNFun n a b - > ArityNFun nab
listApply _ = id
three :: Int
three = listApply p2（+）2 1
oof :: String
oof = listApply p1 reversefoo
true :: Bool
true = listApply p0 True
showplus :: Int - > Int - > String
showplus xy = show（x + y）
zero :: String
zero = listApply p2 showplus 0 0
这里我们可以从 GHC.TypeLits Nat >，但是我们需要 UndecidableInstances 。如果你想制作多态版本，这也是可能的，但是索引不是 （n :: Nat）（a :: *）但是（as :: [*]）。对于两种编码，
As an exercise I'm trying to recreate Lisp's apply in Haskell. I do not intend to use this for any practical purpose, I just think it's a nice opportunity to get more familiar with Haskell's type system and type systems in general. (So I am also not looking for other people's implementations.)
My idea is the following: I can use GADTs to "tag" a list with the type of the function it can be applied to. So, I redefine Nil and Cons in a similar way that we would encode list length in the type using a Nat definition, but instead of using Peano numbers the length is in a way encoded in the tagging function type (i.e. length corresponds to the number of arguments to the function).
Here is the code I have so far:
{-# 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
In the last line, my idea would be that (+) will be of type Int -> Int -> Int, where Int -> Int corresponds to the n in (n -> o) and o corresponds to the last Int (the output) [1]. As far as I can tell, this type seems to work out with the type of my argsN definitions.
However, I get two errors, of which I will state the component that seems relevant to me:
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’
and
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’
I'm not sure how to interpret the first error. The second error is confusing me since it does not match with my interpretation stated marked with [1] earlier.
Any insights into what is going wrong?
P.S: I'm more than willing to learn about new extensions if that would make this work.
You got it almost right. Recursion should follow the structure of 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))
Must say, that this looks quite elegant!
Even OP doesn't ask for other's people implementation. You can approach problem a bit differently, resulting in a different looking but neat 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
Here we could use Nat from GHC.TypeLits, but then we'd need UndecidableInstances. The added sugar is not worth the trouble in this example.
If you want to make polymorphic version, that's also possible, but then index is not (n :: Nat) (a :: *) but (as :: [*]). Also making plusN could be a nice exercise, for both encodings.
这篇关于使用GADT在Haskell中重新创建Lisp的`apply'的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
