Generieren Sie die Funktion der gegebenen Arität in Haskell mithilfe von Typzahlen

Question

Angenommen, ich habe die natürlichen Zahlen in Haskell -Typen codiert und habe eine Möglichkeit, sie hinzuzufügen und zu subtrahieren:

data Zero
data Succ n
-- ...

Ich habe verschiedene Code -Bits gesehen, die das Erscheinungsbild variadischer Funktionen erzeugen, wie z. Dies, was das Folgende ermöglicht:

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

Ich frage mich, ob ich das aufbauen kann, um eine Funktion zu erstellen, die nur die Anzahl der Argumente akzeptiert, die einer Instanz einer Typzahl entsprechen. Was ich versuche zu tun, würde ungefähr aussehen wie:

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

Ich bin mir bewusst, dass dies ziemlich albern ist und dass es wahrscheinlich eine Zeitverschwendung ist, aber es schien etwas, was Spaß am Wochenende machen würde.

Answer 1

OK. Ja. Auf jeden Fall, indem Sie einen numerischen Typ um die rekursiven Instanzen einleiten.

Erstens etwas Kesselplatte:

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

Deine Nats:

data Zero
data Succ n

Ein rekursiver Baumeister für die variadischen Funktionen, jetzt mit einem n Streit:

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

Ein Basisfall: Halten Sie an, wenn wir ankommen Zero:

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

Ansonsten um einen und wieder aufnehmen:

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

Jetzt wollen wir nur noch dreimal schleifen, also schreiben Sie das auf:

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

Fertig.

Testen:

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

Alle weniger oder mehr sind Fehler:

*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

Ich sehe Ihre Funktionsabhängungs-Multiparameter mit leerem Datendaten flexibel abgeschottete Typvariablen und erhöhe Ihnen eine Haskell 98-Version! Es verwendet Holeymonoid, das bei Hackage erhältlich ist:

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

Tests (zögern Sie nicht, alle Typ -Signaturen wegzulassen):

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

Answer 3

Das Einbinden von Martijns Code ergibt eine sehr einfache Lösung:

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

Answer 4

Oh mein ... flexiblecontexts ??? Nomonomorphismreestriction ??? Komm schon, Jungs, ist es nicht genau das, wofür Schriftstellungen da sind?

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