Можно ли ввести в Haskell функцию с переменным числом аргументов?

Обратите внимание на следующий термин Haskell:

callNTimes :: forall a . Int -> (a -> a) -> a -> a
callNTimes n f 0 = x
callNTimes n f x = f (callNTimes (n-1) f x)

firstOf :: ??????
firstOf n = callNTimes n (\ x y -> x)

Если мы игнорируем типы и нормализуем функции вручную, firstOf - это функция, которая получает N, затем N аргументы, отбрасывает все, кроме первого, и возвращает его. firstOf 3 10 20 30 возвращает 3. Можно ли ввести эту функцию в GHC 8.0 с новыми функциями зависимой типизации?


types haskell dependent-type
person MaiaVictor    schedule 27.01.2016    source источник
comment
Вы пробовали очевидный типовой подход? (с литералами уровня типа или без них)   -  person Random Dev    schedule 27.01.2016
comment
Для меня это не очевидно, не могли бы вы порекомендовать какой-нибудь ресурс для изучения этого подхода?   -  person MaiaVictor    schedule 27.01.2016
comment
возможно, это слово было выбрано неудачно - насколько мне известно, вы можете думать о семействе типов как о карте между типами, и, похоже, вам нужно именно это здесь, чтобы получить тип для части ??? - я постараюсь что-нибудь придумать позже (и, вероятно, я не вижу очевидного места, где это не удастся)   -  person Random Dev    schedule 27.01.2016
comment
Для меня это имеет смысл, так что семейства типов - это в основном функции, варьирующиеся от типов? Проблема в том, что я вообще не знаю, как они работают. Спрошу у друга гугла.   -  person MaiaVictor    schedule 27.01.2016
comment
Каноническим примером вариативной функции является printf.   -  person leftaroundabout    schedule 27.01.2016
comment
@Viclib, семейства типов - это просто функции уровня типов в мире с независимыми типами.   -  person user3237465    schedule 27.01.2016
comment
@jberryman, это не дубликат, поскольку OP явно спрашивает о зависимо типизированном решении.   -  person user3237465    schedule 27.01.2016
comment
Вы имеете в виду callNTimes 0 f x = x и callNTimes n f x = f (callNTimes (n-1) f x)? Я слишком далек от понимания callNTimes, чтобы превратить этот комментарий в предложение редактирования.   -  person Franky    schedule 27.01.2016
comment
да. Я понятия не имею, почему у меня была неправильная версия, поскольку она верна в моем файле lcoal ...   -  person MaiaVictor    schedule 27.01.2016
comment
Я создал репозиторий примеров поливариадических функций и способов их создания, что я сказать проверить.   -  person AJF    schedule 27.01.2016
comment
См. Также Как определить применение Lisp в Haskell?.   -  person Daniel Wagner    schedule 27.01.2016

Ответы (2)


arrow_upward
5
arrow_downward

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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Variadic where

data Z a = Z
data S t a = S (t a)

class Var n where
  type El n :: *
  type Res n :: *
  firstOf :: n -> El n -> Res n

instance Var (Z a) where
  type El (Z a) = a
  type Res (Z a) = a
  firstOf Z a = a

instance (El (n a) ~ a, Var (n a)) => Var (S n a) where
  type El (S n a) = a
  type Res (S n a) = a -> Res (n a)
  firstOf (S n) a _ = firstOf n a

Вот несколько примеров:

λ> firstOf Z 5
5
λ> firstOf (S Z) 5 9
5
λ> firstOf (S (S Z)) 5 8 9
5
λ> firstOf (S (S Z)) "Hi" "World" "Uhu"
"Hi"

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

примечания

  • он использует S и Z как простую замену * литералам уровня типа, и вы, вероятно, сможете заставить его работать с этим
  • версия firstOf (S (S Z)), в которой вы ожидаете, что 2 аргумента ожидают 3 - это потому, что я начинаю с Z = 1 аргумент
  • Я только что увидел, что вам нужно firstOf 3 10 20 30 = 3, чего не будет (это даст 10) - что, вероятно, выполнимо с литералами уровня типа и очевидной перегрузкой.
person Random Dev    schedule 27.01.2016
comment
Я бы использовал семейства закрытого типа, например здесь. Не уверен, будет ли лучше. - person user3237465; 27.01.2016
comment
@ user3237465 ... только что видел (и все еще пытаюсь понять) - person Random Dev; 27.01.2016

arrow_upward
2
arrow_downward 

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

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)

constN :: SL as -> b -> Fun as b
constN  Sn    y = y
constN (Sc s) y = \_ -> constN s y

-- 1
main = print $ constN (Sc (Sc (Sc Sn))) 1 "a" [3] True

Например. Fun [Int, Bool] [Int] = Int -> Bool -> [Int]. SL - это синглтон, который позволяет поднять списки до уровня типа. Сопоставление с образцом на SL as показывает, что as либо [], либо a:as. В первом случае цель имеет тип Fun [] b, а это просто b. Во втором случае цель имеет тип a -> Fun as b, отсюда и лямбда.

И простое решение всего за GADTs:

{-# LANGUAGE GADTs #-}

data T z a where
    Tz :: T z z
    Ts :: T z b -> T z (a -> b)

constN :: T z a -> z -> a
constN  Tz    y = y
constN (Ts s) y = \x -> constN s y

-- 1
main = print $ constN (Ts (Ts (Ts Tz))) 1 "a" [3] True
person user3237465    schedule 27.01.2016
comment
@Carsten, я добавил решение попроще. Однако в этом случае, вероятно, лучше использовать классы типов, такие как здесь или здесь. - person user3237465; 27.01.2016