Last active
December 5, 2024 20:04
-
-
Save sciolizer/411e96c1a8ae20c5fe8bad64b58be2e9 to your computer and use it in GitHub Desktop.
A haskell puzzle about representing functions with various arities.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Suppose we have the following expression type for a dynamically typed language | |
| data Value | |
| = VNull | |
| | VInt Int | |
| | VString String | |
| | VNative NativeFunction | |
| data NativeFunction = NativeFunction Int ([Value] -> IO Value) | |
| arity :: NativeFunction -> Int | |
| arity (NativeFunction a _) = a | |
| -- if not enough values are supplied, returns Nothing | |
| -- if correct number of values are supplied, returns Just (<the action>, []) | |
| -- if too many values are supplied, returns Just (<the action>, <excess values>) | |
| invoke :: NativeFunction -> [Value] -> Maybe (IO Value, [Value]) | |
| invoke (NativeFunction a f) vals | |
| | length vals < a = Nothing | |
| | otherwise = let (inputs, excess) = splitAt a vals in Just (f inputs, excess) | |
| nativeReadLn :: NativeFunction | |
| nativeReadLn = NativeFunction 0 impl | |
| where | |
| impl [] = VString <$> readLn | |
| impl _ = error "interpreter bug: wrong number of arguments" | |
| nativePrint :: NativeFunction | |
| nativePrint = NativeFunction 1 (\args -> VNull <$ impl args) | |
| where | |
| impl [VNull] = print "null" | |
| impl [VInt i] = print i | |
| impl [VString s] = print s | |
| impl [VNative _] = print "<native function>" | |
| impl _ = error "interpreter bug: wrong number of arguments" | |
| nativePlus :: NativeFunction | |
| nativePlus = NativeFunction 2 impl | |
| where | |
| impl [VInt a, VInt b] = return . VInt $ a + b | |
| impl [_, _] = ioError (userError "invalid argument types to plus (+)") | |
| impl _ = error "interpreter bug: wrong number of arguments" | |
| -- All of the native functions have this annoying wildcard case where they error out with | |
| -- "interpreter bug: wrong number of arguments." | |
| -- The wildcard case is unreachable because the 3 native functions are honest and correct about | |
| -- their arity, and because `invoke` always passes the right number of arguments. | |
| -- But the wildcard case could still be hit if any of these 4 functions were buggy, or if some other | |
| -- code were later written that pattern matched on NativeFunction and invoked it with the wrong | |
| -- number of arguments. | |
| -- Can we come up with an alternative definition of NativeFunction that makes it | |
| -- 1. impossible to invoke with the wrong number of arguments, and | |
| -- 2. impossible for any instance of `NativeFunction` to lie about its arity? | |
| -- | |
| -- (Do not try to remove the "invalid argument types to plus (+)", which is correct behavior | |
| -- for an interpreter of a dynamically typed language. Only focus on removing the | |
| -- "interpreter bugs"s) | |
| -- | |
| -- Scroll down for a hint. | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- Hint #1: | |
| -- The following definition is impossible to invoke with the wrong number of arguments. | |
| data NativeFunctionHint1 | |
| = ZeroHint1 (IO Value) | |
| | SuccHint1 (Value -> NativeFunctionHint1) | |
| -- which solves problem #1. But now we've kind of lost the ability to implement `arity`. | |
| -- We could hack it like this: | |
| arityHint1 :: NativeFunctionHint1 -> Int | |
| arityHint1 (ZeroHint1 _) = 0 | |
| arityHint1 (SuccHint1 f) = 1 + arityHint1 (f VNull) | |
| -- but now we're implicitly assuming that native functions won't check their argument types | |
| -- until the last moment. The following implementation of nativePlus is compatible: | |
| nativePlusHint1 :: NativeFunctionHint1 | |
| nativePlusHint1 = SuccHint1 (\left -> SuccHint1 (\right -> ZeroHint1 (impl left right))) | |
| where | |
| impl (VInt a) (VInt b) = return . VInt $ a + b | |
| impl _ _ = ioError (userError "invalid argument types to plus (+)") | |
| -- but the following implementation fools us into thinking its arity is 1, when it's actually 2: | |
| dishonestNativePlus :: NativeFunctionHint1 | |
| dishonestNativePlus = SuccHint1 cheat | |
| where | |
| cheat VNull = ZeroHint1 (return . VInt $ 5) | |
| cheat left = SuccHint1 (\right -> ZeroHint1 (impl left right)) | |
| impl (VInt a) (VInt b) = return . VInt $ a + b | |
| impl _ _ = ioError (userError "invalid argument types to plus (+)") | |
| -- How do we solve problem #2, that of making sure native functions cannot lie about their arity? | |
| -- Scroll down for more hints. | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- Hint #2: | |
| -- Consider parameterizing NativeFunction to make it work for arbitrary types, e.g. | |
| -- data NativeFunction x = .. | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- Hint #3: | |
| -- () is one way to represent a "null" value that cannot be pattern matched, which would solve our | |
| -- arity problem. Scroll down for the core of the solution. | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- Core of the solution: | |
| data ValueSol | |
| = VNullSol | |
| | VIntSol Int | |
| | VStringSol String | |
| | VNativeSol NativeFunctionSol | |
| newtype NativeFunctionSol = NativeFunctionSol {runNF :: forall x. NativeFunctionSolImpl x} | |
| data NativeFunctionSolImpl x | |
| = Zero ((x -> ValueSol) -> IO ValueSol) | |
| | Succ (x -> NativeFunctionSolImpl x) | |
| -- Scroll down for the explanation of Zero and Succ, and why we're using a forall. | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- The "forall x" is a "lambda", but at the type level (and usually inferred by ghc so you don't | |
| -- have to type it out). It has different effects depending on whether you are "introducing" an | |
| -- instance of NativeFunctionSol (i.e. calling its constructor) of you are "eliminating" an instance | |
| -- of NativeFunctionSol (i.e. pattern matching). | |
| -- | |
| -- If you are constructing a NativeFunctionSol (i.e. you are nativeRead, nativePrint, or nativePlus), | |
| -- then your instance must contain a "lambda" that "inputs" a type x "at runtime" (though no actual | |
| -- substitution occurs at runtime). Since the type x is not received until "runtime", none of the | |
| -- code in nativeRead, nativePrint, or nativePlus can make assumptions about its value. The value of | |
| -- x is "uninterpretable", and so the native functions can only create NativeFunctionsSols that work | |
| -- for arbitrary x's.) | |
| -- | |
| -- Because x is uninterpretable, we can input Values directly into Succ, still | |
| -- knowing that introducers cannot introspect them. The only thing they can do is hold onto | |
| -- the values. They don't gain introspection ability until eliminating code gives them an "unwrap" | |
| -- function (x -> Value), which the eliminator can't do until it reaches the Zero constructor. | |
| -- | |
| -- The `invoke` function (an eliminator) passes `Value` (the type) to the forall-lambda, and the | |
| -- so called "unwrap" function given to Zero is just the identity function. | |
| -- | |
| -- The `arity` function (also an eliminator) can pass any ground type to the forall-lambda, | |
| -- since it has no intention of ever unwrapping the stub "Values" it gives to Succ. | |
| -- | |
| -- At this point I highly recommend trying to implement arity, invoke, nativeRead, nativePrint, and | |
| -- nativePlus using this definition of NativeFunctionSol, but you can keep scrolling if you want | |
| -- to see the complete solution. | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- Rest of the solution: | |
| -- arity uses () as a "null value", but unlike VNull, native functions are not able to | |
| -- pattern match on it, because they cannot assume that x = () | |
| aritySol :: NativeFunctionSol -> Int | |
| aritySol (NativeFunctionSol inner) = arity' inner | |
| where | |
| arity' (Zero _) = 0 | |
| arity' (Succ f) = 1 + arity' (f ()) | |
| -- actually, we could use any ground type we want, because the crucial thing is that native | |
| -- functions don't know what x is! The following goofy implementation uses [Value], but is also | |
| -- correct, and still meets all of our criteria: | |
| goofyAritySol :: NativeFunctionSol -> Int | |
| goofyAritySol (NativeFunctionSol inner) = goofyAritySol' inner | |
| where | |
| goofyAritySol' (Zero _) = 0 | |
| goofyAritySol' (Succ f) = 1 + goofyAritySol' (f [VNullSol, VStringSol "hello moto", VIntSol 7]) | |
| -- () is just a nice choice because it clearly communicates "I don't care about the value" | |
| -- For invoke, we DO care about the value, so we'll pass the Values directly: | |
| invokeSol :: NativeFunctionSol -> [ValueSol] -> Maybe (IO ValueSol, [ValueSol]) | |
| invokeSol (NativeFunctionSol inner) = invokeSol' inner | |
| where | |
| invokeSol' (Zero f) args = Just (f id, args) | |
| invokeSol' (Succ _) [] = Nothing | |
| invokeSol' (Succ f) (a : as) = invokeSol' (f a) as | |
| nativeReadLnSol :: NativeFunctionSol | |
| nativeReadLnSol = NativeFunctionSol $ Zero (\_ -> VStringSol <$> readLn) | |
| nativePrintSol :: NativeFunctionSol | |
| nativePrintSol = NativeFunctionSol $ Succ (\printable -> Zero (\unwrap -> VNullSol <$ impl (unwrap printable))) | |
| where | |
| impl VNullSol = print "null" | |
| impl (VIntSol i) = print i | |
| impl (VStringSol s) = print s | |
| impl (VNativeSol _) = print "<native function>" | |
| nativePlusSol :: NativeFunctionSol | |
| nativePlusSol = NativeFunctionSol $ Succ (\left -> Succ (\right -> Zero (\unwrap -> impl (unwrap left) (unwrap right)))) | |
| where | |
| impl (VIntSol a) (VIntSol b) = return . VIntSol $ a + b | |
| impl _ _ = ioError (userError "invalid argument types to plus (+)") |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment