Подтвердить что ты не робот

Общий вариант bi f a b = (f a, f b)

Существует ли безопасный тип записи функции

bi f a b = (f a, f b)

чтобы можно было использовать его следующим образом:

x1 :: (Integer, Char)
x1 = bi head [2,3] "45"

x2 :: (Integer, Char)
x2 = bi fst (2,'3') ('4',5)

x3 :: (Integer, Double)
x3 = bi (1+) 2 3.45

? В примерах ранга-типа всегда есть что-то гораздо более простое, чем

g :: (forall a. a -> a) -> a -> a -> (a, a)
g f a b = (f a, f b)
4b9b3361

Ответ 1

Да, хотя и не в Haskell. Но более качественное полиморфное лямбда-исчисление (aka System F-omega) является более общим:

bi : forall m n a b. (forall a. m a -> n a) -> m a -> m b -> (n a, n b)
bi {m} {n} {a} {b} f x y = (f {a} x, f {b} y)

x1 : (Integer, Char)
x1 = bi {\a. List a} {\a. a} {Integer} {Char} head [2,3] "45"

x2 : (Integer, Char)
x2 = bi {\a . exists b. (a, b)} {\a. a} {Integer} {Char} (\{a}. \p. unpack<b,x>=p in fst {a} {b} x) (pack<Char, (2,'3')>) (pack<Integer, ('4',5)>)

x3 : (Integer, Double)
x3 = bi {\a. a} {\a. a} {Integer} {Double} (1+) 2 3.45

Здесь я пишу f {T} для явного приложения типа и предполагаю, что библиотека напечатана соответственно. Что-то вроде \a. a - это лямбда уровня типа. Пример x2 более сложный, так как он также нуждается в экзистенциальных типах, чтобы локально "забыть" другой бит полиморфизма в аргументах.

Вы действительно можете имитировать это в Haskell, указав newtype или тип данных для каждого другого m или n, с которым вы создаете экземпляр, и передаете соответствующим образом завернутые функции f, которые соответственно добавляют и удаляют конструкторы. Но, очевидно, это не весело.

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

swap (x,y) = (y,x)
x4 = bi swap (3, "hi") (True, 3.1)

даже в системе F-omega. Проблема состоит в том, что функция swap более полиморфна, чем bi допускает, и в отличие от x2, в результате не забывается другая полиморфная размерность, поэтому экзистенциальный трюк не работает. Кажется, что вам понадобится такой полиморфизм, чтобы позволить этому (так что аргумент bi может быть полиморфным по разному количеству типов).

Ответ 2

{-# LANGUAGE TemplateHaskell #-}

bi f = [| \a b -> ($f a, $f b)|]

 

ghci> :set -XTemplateHaskell 
ghci> $(bi [|head|]) [2,3] "45" 
(2,'4')

;)

Ответ 3

Даже с ConstraintKinds, я думаю, что барьер будет квантифицировать над "функцией типа" из аргументов к результатам. Вы хотите, чтобы f отображал a -> b и c -> d, и принимал a -> b -> (c, d), но я не думаю, что существует какой-либо способ количественно оценить эту связь с полной общностью.

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

(forall x . cxt x => x -> f x) -> a -> b -> (f a, f b)
 -- e.g. return

(forall x . cxt x => f x -> x) -> f a -> f b -> (a, b)
 -- e.g. snd
(forall x . cxt x => x -> x) -> a -> b -> (a, b)
 -- e.g. (+1)

но учитывая, что вы пытаетесь количественно определить более или менее произвольные функции типа, я не уверен, что вы можете сделать эту работу.

Ответ 4

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

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Data.Function.Bi (bi, Fn(..))

bi :: (Fn i a a', Fn i b b') => i -> a -> b -> (a', b')
bi i a b = (fn i a, fn i b)

class Fn i x x' | i x -> x' where
      fn :: i -> x -> x'

Используйте его так:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, RankNTypes,
             FlexibleInstances, UndecidableInstances #-}
import Data.Function.Bi

data Snd = Snd

instance Fn Snd (a, b) b where
         fn Snd = snd

myExpr1 :: (Int, String)
myExpr1 = bi Snd (1, 2) ("a", "b")
-- myExpr == (2, "b")

data Plus = Plus (forall a. (Num a) => a)

instance (Num a) => Fn Plus a a where
         fn (Plus n) = (+n)

myExpr2 :: (Int, Double)
myExpr2 = bi (Plus 1) (1, 2) (1.3, 5.7)
-- myExpr2 == (3, 6.7)

Это очень неуклюже, но как можно более общее.