Haskellでn番目のパラメータを部分的に適用できますか？

Question

関数、パラメーターの番号、およびそのパラメーターの値をとり、部分的に適用される新しい関数を返す関数apply_nthを書くことができるのではないかと不思議です。

私は、タイプシステムのためにこれは不可能だと感じていますが、私は満足のいく答えを思い付くことができません。私はまた、働くタイプの署名を出すことができません。

言語がよりゆるやかにタイプされていれば、コードはこのように見えると思います。

apply_nth f 0 x = f x 
apply_nth f n x = \a -> apply_nth (f a) (n-1) x 

Answer 1

あなたの気持ちは正しいですが、これは不可能です。部分的なアプリケーションは関数の型を変更し、どのような方法で適用するかによって異なります。しかし、その引数が実行時に余分な引数でのみインデックス付けされている場合、コンパイラは型がどのようになるかを知らず、コンパイラはすべてを型チェックしなければなりません^＆dagger;。実際には、結果にはdependent typeが必要ですが、Haskellは依存型言語ではありません。

実際に、GHCの2つの拡張モジュールを入れて、奇妙なタイプのファミリーを2つ紹介すると、実際にこのような依存型に似たものを実現できます。しかし、正直なところ、これは良い考えだとは思わない。とにかくこれは何が必要ですか？例えば8つのパラメータ以上の関数を扱っているなら、おそらく何か間違っているでしょうし、簡単な関数のために、それぞれが固定引数の位置を1つだけ適用する8つのコンビネータを定義することができます。おそらく妥当だ同様の機能は、引数リストとは異なり

apply_nth :: ([a] -> b) -> Int -> a -> [a] -> b 
apply_nth f i a xs = f $ before ++ [a] ++ after 
where (before, after) = splitAt i xs 

なり、この場合、単一の要素を事前に適用するように、値リストを容易に、長い要素数百することができ、索引付け：あるいは

実行時に意味をなさすことができます。

---

^;_{これは単なる安全上の予防策ではありません。実行時に型が存在しないために必要です。したがって、コンパイラは型に依存する可能性のあるすべての条件を準備する必要があります。これがHaskellが安全である理由です。と簡潔と fast と他の言語のように拡張可能です。}型クラス「魔法」のビットと、

Answer 2

確か：

{-# LANGUAGE DataKinds, KindSignatures, UndecidableInstances #-} 

data Nat = Z | S Nat 

data SNat (n :: Nat) where 
    SZ :: SNat Z 
    SS :: SNat n -> SNat (S n) 

class ApplyNth (n :: Nat) arg fn fn' | n arg fn -> fn', n fn -> arg where 
    applyNth :: SNat n -> arg -> fn -> fn' 

instance ApplyNth Z a (a -> b) b where 
    applyNth SZ a f = f a 

instance ApplyNth n arg' fn fn' => ApplyNth (S n) arg' (arg0 -> fn) (arg0 -> fn') where 
    applyNth (SS n) a f = \a0 -> applyNth n a (f a0) 

applyNthのための一般的なタイプは、それがインデックス（自然数 - タイプでエンコード）かかり、言う、引数を、関数を呼び出し、関数を返します。

2つの機能上の依存関係に注意してください。最初は、インデックス、引数、および入力関数が与えられていると、出力関数の型がわかっていると言います。これは明らかです。 2つ目は、インデックスと入力関数を指定すると、ApplyNthは関数を調べて、必要な引数を見つけ出すことができるということです。

この関数は、型推論とかなりよく果たしている：

>:t \x -> applyNth (SS SZ) x (^) 
\x -> applyNth (SS SZ) x (^) 
    :: (Num fn', Integral b) => b -> fn' -> fn' 
>:t applyNth (SS SZ) 0 (^) 
applyNth (SS SZ) 0 (^) :: Num fn' => fn' -> fn' 
>:t applyNth (SS SZ) (0 :: Integer) (^) 
applyNth (SS SZ) (0 :: Integer) (^) :: Num fn' => fn' -> fn' 
>:t applyNth (SS SZ) ('a' :: Char) (^) 

<interactive>:1:32: Warning: 
    Could not deduce (Integral Char) arising from a use of `^' 
    ... 
applyNth (SS SZ) ('a' :: Char) (^) :: Num fn' => fn' -> fn' 
>let squared = applyNth (SS SZ) 2 (^) 
>:t squared 
squared :: Num fn' => fn' -> fn' 
>squared 3 
9 
>squared 100 
10000 
>let f a b c d e = mapM_ putStrLn 
     [ show n ++ ": " ++ x 
     | (n,x) <- zip [0..] 
      [show a, show b, show c, show d, show e] ] 
>applyNth SZ 'q' $ 
applyNth (SS $ SZ) [1,8,42] $ 
applyNth SZ (True, 10) $ 
applyNth (SS $ SS $ SS SZ) "abcd" $ 
applyNth (SS $ SS $ SS SZ) pi $ 
f 
0: (True,10) 
1: 'q' 
2: [1,8,42] 
3: 3.141592653589793 
4: "abcd" 

また、オペレータの形でそれを定義することができます。

infixl 9 =: 
(=:) :: ApplyNth n arg fn fn' => SNat n -> arg -> fn -> fn' 
(=:) = applyNth 

r = 
SZ =: 'q' $ 
SS SZ =: [1,8,42] $ 
SZ =: (True, 10) $ 
(SS $ SS $ SS SZ) =: "abcd" $ 
(SS $ SS $ SS SZ) =: pi $ 
f 

Answer 3

ない「ハスケル」と呼ばれる任意の言語の内部ではなく、あなたが見れば安全でない関数を含むGlasgow Haskellは、あなたが望むやり方で部分的に適用することができます...引数の場所を正しく指定する必要があります。これはひどいハックです。あなたが非常に快適でない限り、これをしないでください...まあ..これをしないでください。

このコードは、私が似たような質問（Using Typeable to partially apply function at run-time (any time types match)）をしたときのものです。

import Unsafe.Coerce 

testBuild :: String 
testBuild = let f = buildFunc typedFunction ("argument 'b'", 42::Int) 1 
      in f "Look I have applied " " and it seems to work." 

typedFunction :: String -> (String,Int) -> String -> String 
typedFunction = (\a b c -> a ++ show b ++ c) 

buildFunc :: f -> x -> Int -> g 
buildFunc f x 0 = unsafeCoerce f x 
buildFunc f x i = 
     let res = \y -> (buildFunc (unsafeCoerce f y) x (i-1)) 
     in unsafeCoerce res 

そして、出力：我々は引数インデックスを指定

*Main> testBuild 
"Look I have applied (\"argument 'b'\",42) and it seems to work." 

気付いた場合は、（1）誤っプログラムはセグメンテーションフォールト可能性が高いでしょう。

Answer 4

ないという奇妙な形の家族が、超素敵ないか：

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, TypeOperators #-} 

import Data.Proxy 

type family Fun as b where 
    Fun '[]  b = b 
    Fun (a ': as) b = a -> Fun as b 

data SL as where 
    Sn :: SL '[] 
    Sc :: SL as -> SL (a ': as) 

applyN :: Proxy c -> SL as -> Fun as (b -> c) -> b -> Fun as c 
applyN p Sn f y = f y 
applyN p (Sc s) f y = \x -> applyN p s (f x) y 

main = print $ applyN Proxy (Sc (Sc Sn)) zipWith [1,2,3] (-) [6,5,4] -- [5,3,1] 

またSLにProxy cをパッケージ化することができます

data SL as c where 
    Sn :: SL '[] c 
    Sc :: SL as c -> SL (a ': as) c 

applyN :: SL as c -> Fun as (b -> c) -> b -> Fun as c 
applyN Sn f y = f y 
applyN (Sc s) f y = \x -> applyN s (f x) y 

main = print $ applyN (Sc (Sc Sn)) zipWith [1,2,3] (-) [6,5,4] -- [5,3,1] 

それとも、単にいくつかのコンビネータ定義することができます。

を

z = id 
s r f y x = r (f x) y 
applyN = id 

main = print $ applyN (s (s z)) zipWith [1,2,3] (-) [6,5,4] -- [5,3,1]