1

Mind the following Haskell term:

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)

If we ignore the types and normalize the functions by hand, firstOf is a function that receives an N, then N arguments, discards all but the first and returns it. firstOf 3 10 20 30 returns 3. Is it possible to type that function in GHC 8.0 with the new dependent typing features?

MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
  • have you tried the obvious type-family approach? (with or without type level literals) – Random Dev Jan 27 '16 at 13:27
  • It is not obvious to me, would you recommend a resource to learn that approach? – MaiaVictor Jan 27 '16 at 13:29
  • maybe the word was poorly chosen - to my knowledge you can think of type families as a map between types and it seems you need exactly this here to get a type for the `???` part - I will try to work something out later (and probably I don't see the obvious place where this will fail) – Random Dev Jan 27 '16 at 13:30
  • That makes sense to me, so type families are basically functions ranging over types? Issue is, I have no idea how they work at all. I'll ask my friend Google. – MaiaVictor Jan 27 '16 at 13:31
  • 2
    The canonical example of a variadic function is [`printf`](http://hackage.haskell.org/package/base-4.8.2.0/docs/Text-Printf.html#v:printf). – leftaroundabout Jan 27 '16 at 13:40
  • @Viclib, type families are just type-level functions in a non-dependently-typed world. – effectfully Jan 27 '16 at 14:17
  • @jberryman, it's not a duplicate as OP explicitly asks about a dependently typed solution. – effectfully Jan 27 '16 at 14:55
  • Do you mean `callNTimes 0 f x = x` and `callNTimes n f x = f (callNTimes (n-1) f x)`? I am too far from understanding `callNTimes` to turn this comment into an edit suggestion. – Franky Jan 27 '16 at 15:08
  • Yes. I have no idea why I had the wrong version here since it is correct on my lcoal file... – MaiaVictor Jan 27 '16 at 16:44
  • I made a [repository](https://github.com/AJFarmar/haskell-polyvariadic) of examples of polyvariadic functions, and how to make them, that I'd say to check out. – AJF Jan 27 '16 at 17:47
  • See also [How do I define Lisp’s apply in Haskell?](http://stackoverflow.com/q/6168880/791604). – Daniel Wagner Jan 27 '16 at 18:54

2 Answers2

4

I finally managed to get a working version - it's not exactly what you asked for but it demonstrates what I was commenting about and I think it's quite close

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

here are a few examples:

λ> 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"

if you are interested in how I got there you can check the edit-history

remarks

  • it uses the S and Z as a poor-mansreplacement* for type-level literals and you can probably get it working with this
  • the version firstOf (S (S Z)) which you would expect to want 2 arguments is waiting for 3 - that's because I start with Z = 1 argument
  • I just saw that you wanted firstOf 3 10 20 30 = 3 which this will not do (this will give 10) - which is probably doable with type-level literals and an obvious overload too
Random Dev
  • 51,810
  • 9
  • 92
  • 119
2
{-# 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

E.g. Fun [Int, Bool] [Int] = Int -> Bool -> [Int]. SL is a singleton that allows to lift lists to the type level. Pattern matching on SL as reveals that as is either [] or a:as. In the first case the goal has type Fun [] b which is just b. In the second case the goal has type a -> Fun as b, hence the lambda.

And a simple solution with just 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
effectfully
  • 12,325
  • 2
  • 17
  • 40
  • @Carsten, I added a simpler solution. However in this case it's probably better to use type classes like [here](http://stackoverflow.com/a/33291967/3237465) or [here](http://stackoverflow.com/a/28004372/3237465). – effectfully Jan 27 '16 at 15:22