Characterizing the type of functions that can accept `()` as input (without monomorphizing)

user_2684007 0
Viewed 167

Here are a few simple functions:

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

All of f1, f2, and f3 are able to accept () as an input. On the other hand, of course, f4 can't accept (); f4 () is a type error.

Is it possible to type-theoretically characterize what f1, f2, and f3 have in common? Specifically, is it possible to define an acceptsUnit function, such that acceptsUnit f1, acceptsUnit f2, and acceptsUnit f3 are well-typed, but acceptsUnit f4 is a type error -- and which has no other effect?

The following does part of the job, but monomorphizes its input (in Haskell, and I gather in Hindley-Milner), and hence has an effect beyond simply asserting that its input can accept ():

acceptsUnit :: (() -> a) -> (() -> a)
acceptsUnit = id

-- acceptsUnit f4     ~> error 
-- acceptsUnit f3 'a' ~> error ☹️

The same monomorphizing, of course, happens in the following. In this case, the annotated type of acceptsUnit' is its principal type.

acceptsUnit' :: (() -> a) -> (() -> a)
acceptsUnit' f = let x = f () in f
system-f type-theory hindley-milner polymorphism haskell
1 Answers

It's easy to type-theoretically characterize what f1, f2, and f3 but not f4 have in common. In the language of Hindley-Milner, the first three have polytypes that can be specialized to a polytype of the form:

forall a1...an. () -> tau

for n >= 0 and tau an arbitrary monotype. The fourth one can't.

Can you write a function that accepts the first three as an argument but rejects the fourth? Well, it depends on the type system you're using and the latitude you have to structure your function. In the usual Hindley-Milner and/or standard Haskell type system, if you have latitude to pass two copies of your candidate function to the acceptance function, the following will work:

acceptsUnit :: (() -> a) -> (b -> c) -> (b -> c)
acceptsUnit = flip const

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

main = do
  print $ acceptsUnit f1 f1 ()
  print $ acceptsUnit f2 f2 10
  print $ acceptsUnit f3 f3 10
  -- print $ acceptsUnit f4 f4  -- type error

That's probably the best you'll be able to do with standard Haskell (and probably the best you can do with Haskell plus GHC type system extensions, or someone would have found something by now).

If you're free to define your own typing system with its own typing rules, then the sky is the limit.

user_72030160
Related