Генерировать функцию заданной arity в Haskell с использованием номеров типов

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

data Zero
data Succ n
-- ...

Я видел различные биты кода, которые создают появление вариационных функций, таких как this, что позволяет:

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

Я знаю, что это довольно глупо и что это, вероятно, пустая трата времени, но казалось, что это будет весело для выходных.

Ответ 1

OK. Да. Определенно, путем потоковой передачи числового типа вокруг рекурсивных экземпляров.

Во-первых, некоторый шаблон:

{-# 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

В противном случае, декремент на единицу и рекурсия:

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]])

Ответ 2

Я вижу ваш многопараметрический многофактор с параметрами-зависимыми типами с гибким охватом переменных типа и повышаю версию Haskell 98! Он использует HoleyMonoid, который доступен для взлома:

{-# 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"]

Ответ 3

Вставка кода Martijn дает очень простое решение:

zero xs = xs
suc n xs x = n (xs ++ [x])
buildList n = n []

Ответ 4

О, мой... FlexibleContexts??? NoMonomorphismRestriction??? Да ладно, ребята, разве это не то, для чего предназначены TypeFamilies?

{-# LANGUAGE TypeFamilies #-}
data Zero = Zero
newtype Succ n = Succ n
zero = Zero
one = Succ zero
two = Succ one
three = Succ two
class BuildList n where
    type BL n
    buildListPrefix :: n -> ([String] -> [String]) -> BL n
instance BuildList Zero where
    type BL Zero = [String]
    buildListPrefix Zero h = h []
instance BuildList n => BuildList (Succ n) where
    type BL (Succ n) = String -> BL n
    buildListPrefix (Succ n) h s = buildListPrefix n (h . (s:))
buildList:: BuildList n => n -> BL n
buildList n = buildListPrefix n id