# acme-smuggler

Ben Clifford

benc@hawaga.org.uk

Press 's' for speaker notes

``````
smuggle :: Typeable a =>   a -> ()
discover :: Typeable a => () -> Maybe a
```
```

This is impossible. But it is possible.

## Demo

```> import Acme.Smuggler
> let x = smuggle (32 :: Float)
> let y = smuggle "Hello"
> :t x
x :: ()
> :t y
y :: ()
> discover x :: Maybe Float
Just 32.0
> discover x :: Maybe String
Nothing
> discover y :: Maybe String
Just "Hello"
```

## Injecting

``````
type T = Either String Int
``````
``````
inj = Left :: String -> T
``````

## Projecting

``````
prj :: T -> Maybe String
prj = either Just (const Nothing)
``````
```> prj (inj "hi")
Just "hi"

> prj (Right 123)
Nothing
```

## prj . int round trip rule

``````
(prj . inj) = Just
``````

## Other examples

Open unions:

``type S = Union '[Char, Int, [()]]``

`Word8` into `Double`:

```> fromIntegral (255 :: Word8) :: Double
255.0

> round (255.0 :: Double) :: Word8
255
> round (3.1415 :: Double) :: Word8
3
```

`read . show`

## Cardinality

``````
type T = Either String Int

inj :: String -> T
inj = Left
```
```

Injection rule:

```inj a == inj b => a == b
```

https://en.wikipedia.org/wiki/Cardinality

```smuggle :: a -> ()
discover :: () -> Maybe a
```
or lets rename and specialise:
```inj :: String -> ()
prj :: () -> Maybe String
```

Can an injection exist?

Can `inj :: String -> ()` exist?

```inj "hello" = ()
inj "goodbye" = ()
```

Injection rule:

`() == () => "hello" == "goodbye"`

... doesn't hold

So acme-smuggler is impossible!

... but it isn't impossible. Everything I've just told you is wrong.

## Getting dirty

``````
type T = Either String Int

fromLeft :: T -> String
fromLeft (Left s) = s
``````
```fromLeft (Right 7) = ??????
```
``````
type T = Either String Int

fromLeft :: T -> String
fromLeft (Left s) = s
fromLeft (Right _) = undefined
``````

## Smuggling `Bool`

``````
inj :: Bool -> ()
inj True = ()
inj False = undefined
``````

## Laziness

```> let x = inj False
-- no error
> (const 3) x
3
> x
*** Exception: Prelude.undefined
```

## human-prj

```> inj True
()
> inj False
*** Exception: Prelude.undefined
```

but...

```case x of
() -> True
???? -> False

if x == undefined then False else True
```

## Observing bottom programmatically

``````
try :: IO a -> IO (Either e a)

h :: () -> IO (Either SomeException Bool)
h v = try \$ pure (v == ())

prj' :: () -> IO Bool
prj' v = case h v of
Right _ -> True
Left _ -> False
``````
``````
unsafePerformIO :: IO a -> a

prj :: () -> Bool
prj = unsafePerformIO . prj'
``````

## Is unsafePerformIO safe here?

Is this referentially transparent? YES

Can execute this multiple times (or no times?) YES

For this to be safe, the IO computation should be free of side effects and independent of its environment.

## Boolean Smuggler

``````
inj :: Bool -> ()
prj :: () -> Bool

(prj . inj) = id

-- ????
inj a == inj b => a == b
``````

## Extensible exceptions

``````
h :: () -> IO (Either SomeException Bool)
h v = try \$ pure (v == ())

prj' v = case h v of
Right _ -> True
Left _ -> False
``````
``````
class Exception where ...

instance Exception IOException
instance Exception BlockedIndefinitelyOnSTM
instance Exception AssertionFailed
instance Exception PatternMatchFail

instance Exception SomethingToSmuggle - ????
``````

## Data.Dynamic

``````
toDyn :: Typeable a => a -> Dynamic -- aka inj
fromDynamic :: Typeable a	    -- aka prj
=> Dynamic -> Maybe a
``````
``````
instance Exception Dynamic
``````

## Putting the pieces together

``````
-- inj
smuggle :: Typeable t => t -> ()
smuggle = throw . toDyn

-- prj
discover :: Typeable t => () -> Maybe t
discover = either (fromDynamic) (const Nothing)
. unsafePerformIO
. try
. (pure \$!)
``````
``````
smuggle :: Typeable t => t -> ()
smuggle = throw  .  toDyn
--     ()  <-   Dyn   <-   t
--     a
``````
``````
discover :: Typeable t => () -> Maybe t
discover =
either (fromDynamic) (const Nothing) -- Maybe t
. unsafePerformIO              -- Either Dynamic ()
. try                          -- IO (Either Dynamic ())
. (pure \$!)                    -- IO ()
-- ()
``````
- fin -