Блог

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

 data Zero
data Succ n
-- ...
  

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

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

Мне интересно, могу ли я на основе этого создать функцию, которая будет принимать только то количество аргументов, которое соответствует экземпляру типа number. То, что я пытаюсь сделать, выглядело бы примерно так:

 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
  

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

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

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

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

Ваши nats:

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

Я вижу, что ваш многопараметр функциональной зависимости пуст, а переменные типа с гибким типом данных имеют ограниченную область действия, и предлагаю вам версию 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"]
  

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

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

О, боже… Гибкие тексты??? Ограничение номономорфизма??? Да ладно, ребята, разве это не именно то, для чего существуют семейства типов?

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