Menu
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
410
The simplest way to describe a function is with a function type expression . These types are syntactically similar to arrow functions: console. log ( s ); The syntax (a: string) => void means “a function with one parameter, named a, of type string, that doesn’t have a return value”.
You can pass integers, floats, string, boolean etc values to a function as an argument. For example, if a function returns sum of two numbers then you can pass two numbers ,either integer or float as an argument. Can someone help me with defining a function that takes up an argument?
This is useful when describing function types because you can describe functions that accept any value without having any values in your function body. Conversely, you can describe a function that returns a value of unknown type: return JSON. parse ( s ); // Need to be careful with 'obj'! The never type represents values which are never observed.
Writing generic functions is fun, and it can be easy to get carried away with type parameters. Having too many type parameters or using constraints where they aren’t needed can make inference less successful, frustrating callers of your function.
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.
69
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
