Why type systems matter

TL;DR

A fistful of formal methods

01 |    let module1 = {
02 | defaultValidators: [
03 | (x) => 2 == x.split(' ').length,
04 | ],
05 | validate: (input) => (fs) =>
06 | fs.reduce((acc, f) => acc && f(input), true),
07 | };
08 |
09 | let module2 = {
10 | alsoCapitalised: [
11 | (x) =>
12 | x.split(' ').reduce(
13 | (acc, x) => acc && (/[A-Z]/.test(x[0])), true
14 | )
15 | ] + module1.defaultValidators,
16 | }
17 |
18 | let main = {
19 | main: (input) => {
20 | let validators = module2.alsoCapitalised;
21 | if (module1.validate(input)(validators)) {
22 | console.log("It's time to open the door");
23 | }
24 | }
25 | }
26 |
27 | main.main("Viktor Tsoi");
Uncaught TypeError: fs.reduce is not a function
validate debugger eval code:6
main debugger eval code:21
<anonymous> debugger eval code:27
15 | ].concat(module1.defaultValidators),
It's time to open the door
01 | {-# LANGUAGE OverloadedStrings #-}
02 | import qualified Data.Text as T
03 | import Data.Text( Text )
04 | import Data.Char( isUpper )
05 |
06 | defaultValidators :: [Text -> Bool]
07 | defaultValidators = [\x -> 2 == (length $ T.splitOn " " x)]
08 |
09 | validate :: Text -> [Text -> Bool] -> Bool
10 | validate input fs = foldl (\acc f -> acc && f input) True fs
11 |
12 | alsoCapitalised :: [Text -> Bool]
13 | alsoCapitalised = [\x -> foldl (\acc w -> acc && (isUpper $ T.head w))
14 | True
15 | (T.splitOn " " x)] + defaultValidators
16 |
17 | main :: IO ()
18 | main =
19 | case validate input defaultValidators of
20 | True -> putStrLn "It's time to open the door"
21 | _ -> putStrLn "Close the door behind me"
22 | where
23 | input = "Viktor Tsoi"
/tmp/hi.hs:13:19: error:
No instance for (Num [Text -> Bool]) arising from a use of '+'
15 | (T.splitOn " " x)] ++ defaultValidators

Benefits of using type systems

/tmp/hi.hs:19:3: error: [-Wincomplete-patterns, -Werror=incomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: False
|
19 | case validate input defaultValidators of
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
data PKC pass sk pk slip sig sigmsg enc plain cipher = PKC
{ -- | Initial key derivation function
kdf :: pass -> (sk, pk, slip),
-- | Rederive with kdf
rekdf :: slip -> pass -> (sk, pk),
-- | Sign data with key @sk@ and produce a detached @signature@
-- possibly containing @pk@ for verification.
sign :: sigmsg -> (sk, pk) -> signature pk,
-- | Verifies @signature@ container's validity.
verify :: sigmsg -> signature pk -> Bool,
-- | Encrypt data of type @plain@ to the key @pk@ and produce @encrypted@
-- containing @cipher@.
encrypt :: plain -> pk -> encrypted pk cipher,
-- | Decrypts @cipher@, contained in an @encrypted@ container into @plain@.
decrypt :: encrypted pk cipher -> sk -> Maybe plain
}
data DummyTag = DummySK | DummyPK | DummySlip
deriving (Show, Eq)

-- | Note that we abuse the fact that in dummy implementation
-- secret key and public key are both represented with a
-- DummyTagged type alias to embed secret key together with
-- the message.
newtype DummySigned msg key = DummySigned {sig :: (key, (key, msg))}
deriving (Show, Eq)

-- ...

type DummyTagged = (DummyTag, ByteString)

-- ...

dummyKdf :: ByteString -> IO (Maybe (DummyTagged, DummyTagged, DummyTagged))
dummyKdf pass = pure $ Just ((DummyPK, pass), (DummySK, pass), (DummySlip, pass))

dummyRekdf :: DummyTagged -> ByteString -> Maybe (DummyTagged, DummyTagged)
dummyRekdf (DummySlip, x) pass =
go (x == pass)
where
go True = Just ((DummyPK, pass), (DummySK, pass))
go False = Nothing
dummyRekdf _ _ = error "DummySlip expected in the 1st argument"

-- ...

dummySign :: (DummyTagged, DummyTagged) -> msg -> DummySigned msg DummyTagged
dummySign (verificationKey@(DummyPK, _), signingKey@(DummySK, _)) blob =
DummySigned (verificationKey, (signingKey, blob))
dummySign _ _ = error "The first argument has to be a tuple of DummySK and DummyPK"

-- | Note that we're not comparing public key with secret key
-- but rather compare embedded bytestrings which match if the keys
-- were derived from the same password by kdf
dummyVerify :: Eq a => DummySigned a DummyTagged -> a -> Bool
dummyVerify (DummySigned ((DummyPK, signedAs), ((DummySK, signedWith), signedWhat))) candidate =
(signedAs == signedWith) && (candidate == signedWhat)
Prelude> :t foldl foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b

Drawbacks of type systems

Bottom line

--

--

Educate, explore and empower. Concisely. Doma.dev

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store