使用类型编号在Haskell中生成给定arity的函数

Question

假设我已经编码了Haskell类型中的自然数,并且我有一种方法可以添加和减去它们:

data Zero
data Succ n
-- ...

我已经看到其产生的可变参数的功能,如外观的码的各个位,这个,这允许以下内容:

buildList "polyvariadic" "function" "wut?" :: [String]
-- ["polyvariadic","function","wut?"]

我想知道的是,我是否可以构建一个只接受与类型号实例对应的参数数量的函数.我想做的事情看起来像:

one = Succ Zero
two = Succ one
three = Succ two

threeStrings :: String -> String -> String -> [String]
threeStrings = buildList three

threeStrings "asdf" "asdf" "asdf"
-- => ["asdf","asdf","asdf"]

threeStrings "asdf"
-- type checker is all HOLY CHRIST TYPE ERROR

threeStrings "asdf" "asdf" "asdf" "asdf"
-- type checker is all SWEET JESUS WHAT YOU ARE DOING

我知道这是非常愚蠢的,这可能是浪费我的时间,但它看起来像周末会很有趣.

Answer 1

好.是.当然,通过在递归实例周围线程化数字类型.

首先,一些样板:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE EmptyDataDecls         #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE ScopedTypeVariables    #-}

你的自然:

data Zero
data Succ n

可变参数函数的递归构建器,现在带有n参数:

class BuildList n a r | r -> a where
    build' :: n -> [a] -> a -> r

一个基本案例:当我们到达时停止Zero:

instance BuildList Zero a [a] where
    build' _ l x = reverse $ x:l

否则,递减1并递归:

instance BuildList n a r => BuildList (Succ n) a (a->r) where
    build' (_ :: Succ n) l x y = build' (undefined :: n) (x:l) y

现在,我们只想循环3次,所以写下来:

build :: BuildList (Succ (Succ Zero)) a r => a -> r
build x = build' (undefined :: Succ (Succ Zero)) [] x

完成.

测试:

> build "one" "two" "three" :: [[Char]]
["one","two","three"]

任何更少或更多的错误:

*Main> build "one" "two" "three" "four" :: [[Char]]

<interactive>:1:1:
    No instance for (BuildList Zero [Char] ([Char] -> [[Char]]))

*Main> build "one" "two" :: [[Char]]

<interactive>:1:1:
    No instance for (BuildList (Succ Zero) [Char] [[Char]])

Answer 2

我看到你的函数依赖多参数empty-datatype灵活范围的类型变量,并提出一个Haskell 98版本!它使用HoleyMonoid,它可以在hackage上使用:

{-# LANGUAGE NoMonomorphismRestriction #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.HoleyMonoid

suc n = later (:[]) . n

zero  = id
one   = suc zero
two   = suc one
three = suc two

buildList = run

测试(随意省略任何类型的签名):

> run three "one" "two" "three"
["one","two","three"]