使用类型数字在Haskell中生成给定元素的函数 [英] Generate function of given arity in Haskell using type numbers

问题描述

假设我已经在Haskell类型中编码了自然数，并且我有一种加法和减法的方法：

  data zero 
 data Succ n 
  -  ... 
  

我有看到了创建可变参数函数外观的各种代码，比如这个，它允许以下内容：

  buildListpolyvariadicfunctionwut？ :: [String] 
  -  [polyvariadic，function，wut？] 
  

我想知道的是，我是否可以构建一个函数，只接受与类型编号实例相对应的参数个数。我想要做的是这样的：

  one = Succ零
 two = Succ one 
 three = Succ two 
 
 threeStrings :: String  - >字符串 - >字符串 - > [String] 
 threeStrings = buildList三
 
 threeStringsasdfasdfasdf
  -  => [asdf，asdf，asdf] 
 
 threeStringsasdf
  - 类型检查器全是圣诞节类型错误
 
 threeStringsasdf asdfasdfasdf
  - 类型检查器全部是甜心耶稣你正在做什么
  

我知道这很愚蠢，这可能是浪费我的时间，但它似乎是一件有趣的事情在周末。

解决方案

好的。是。当然，通过在递归实例中对数值类型进行线程化。

首先，一些样板：

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

您的nats：

 数据零
数据Succ n 
  
 
 
 
可变参数函数的递归构建器现在带有一个 n 参数：
  class BuildList nar | r  - > a 
 build':: n  - > [a]  - > a  - > r 
  
基本情况：当我们到达 Zero时停止 
 $ b $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ 
  

否则，减1并递归：

 实例BuildList nar => BuildList（Succ n）a（a-> r）其中
 build'（_ :: Succ n）lxy = build'（undefined :: n）（x：l）y 
  

现在，我们只想循环3次，所以写下来：

  build :: BuildList（Succ（Succ Zero））ar => a  - > r 
 build x = build'（undefined :: Succ（Succ Zero））[] x 
  

测试：

 >建立一二三:: [[Char]] 
 [one，two，three] 
   
 
 
任何更少或更多的错误： 
 
 
  * Main>构建一个两个三个四个:: [[Char]] 
 
< interactive>：1：1：
（BuildList Zero [Char] （[Char]  - > [[Char]]））
 
 * Main>构建onetwo:: [[Char]] 
 
< interactive>：1：1：
（BuildList（Succ Zero）[Char] [[Char ]]）
  
 
Assume I have encoded the natural numbers in Haskell types, and that I have a way of adding and subtracting from them:
data Zero
data Succ n
-- ...
I have seen various bits of code which create the appearance of variadic functions, such as this, which allows the following:
buildList "polyvariadic" "function" "wut?" :: [String]
-- ["polyvariadic","function","wut?"]
What I am wondering is whether I can build off of that to make a function which will only accept the number of arguments that corresponds to an instance of a type number. What I'm trying to do would look something like:
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
I'm aware that this is pretty silly and that it's probably a waste of my time, but it seemed like something that would be fun for the weekend.
解决方案
OK. Yes. Definitely, by threading a numeric type around the recursive instances.


First, some boilerplate:
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE EmptyDataDecls         #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE ScopedTypeVariables    #-}
Your nats:
data Zero
data Succ n
A recursive builder for the variadic functions, now with an n argument:
class BuildList n a r | r -> a where
    build' :: n -> [a] -> a -> r
A base case: stop when we get to Zero:
instance BuildList Zero a [a] where
    build' _ l x = reverse $ x:l
Otherwise, decrement by one and recurse:
instance BuildList n a r => BuildList (Succ n) a (a->r) where
    build' (_ :: Succ n) l x y = build' (undefined :: n) (x:l) y
Now, we only want to loop 3 times, so write that down:
build :: BuildList (Succ (Succ Zero)) a r => a -> r
build x = build' (undefined :: Succ (Succ Zero)) [] x
Done.

Testing:
> build "one" "two" "three" :: [[Char]]
["one","two","three"]
Any less or more are errors:
*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]])


                        
这篇关于使用类型数字在Haskell中生成给定元素的函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！