Year 2015 Day 11
This day provides a gentle introduction to refinement types, types which augment other types with a predicate that must hold for all the values of the refined type, which allow easily defining types as subsets of other types based on some property of the acceptable elements.
While refinement types are quite easy to implement in Idris, and we easily could
implement the one we need for today's task as a throw away data structure just
for this module, we will be using the refined1 library's implementation for
the sake of getting on with it.
import Data.Vect
import Data.String
import Data.Refined.Char
import Util
Data Structures and Parsing
Provide a predicate which establishes that a char is a lowercase alphabetic
character, the only type of character that passwords are allowed to contain. We
use the FromTo predicate from the refined1 library to restrict chars to
within the range from a to z.
This predicate has multiplicity 0, a full discussion of multiplicites and linear types is out of scope for today, but put simply this enforces that a value of this predicate type can be "used" at most 0 times, having the effect of erasing the value at runtime, making this more or less a zero-cost abstraction.
0 IsPasswordChar : Char -> Type
IsPasswordChar = FromTo 'a' 'z'
Combine a Char with its corresponding IsPasswordChar predicate into a
combined "refined" type, whose elements are the subset of Chars that are
lowercase alphabetic characters.
record PasswordChar where
constructor MkPC
char : Char
{auto 0 prf : IsPasswordChar char}
%name PasswordChar pc
A function to fallible convert Chars into refined PasswordChars, this will
return Just if the Char satisfies the predicate, and Nothing otherwise,
aligning with the type-level guarantees of the PasswordChar type.
refineChar : Char -> Maybe PasswordChar
refineChar c = map fromSubset $ refine0 c
where
fromSubset : Subset Char IsPasswordChar -> PasswordChar
fromSubset (Element char prf) = MkPC char
Convenience function returning a as a PasswordChar
lowest : PasswordChar
lowest = MkPC 'a'
"Increment" a PasswordChar, changing it to the next letter (a becomes b,
b becomes c, so on), returning nothing if we go past z, corresponding to a
carry.
We do this by converting the internal Char to an integer, adding one to it,
then converting back to a Char. This low-level conversion loses the refinement
context, forcing us to call refineChar on the new value to bring it back into
the refined type, providing us type-level assurance that this function will
return Nothing if an overflow occurs.
incriment : PasswordChar -> Maybe PasswordChar
incriment (MkPC char) =
let next = chr $ ord char + 1
in refineChar next
A Password is a Vect of 8 PasswordChars. This Vect is sorted in reverse
order compared to the String it corresponds to, with the right-most letter
first, to make implementing the incrimentPassword function a little easier and
cleaner.
We also provide conversion to/from a String
Password : Type
Password = Vect 8 PasswordChar
parsePassword : Has (Except String) fs => String -> Eff fs Password
parsePassword str = do
cs <- note "Password has incorrect number of characters: \{str}"
. toVect 8 . reverse . unpack $ str
cs <- note "Password contained invalid characters: \{str}"
$ traverse refineChar cs
pure cs
passwordToString : Password -> String
passwordToString = pack . toList . reverse . map char
Define a function to increment a Password, this function will "roll over",
producing aaaaaaaa if provided zzzzzzzz.
incrimentPassword : Vect n PasswordChar -> Vect n PasswordChar
incrimentPassword [] = []
incrimentPassword (x :: xs) =
case incriment x of
Nothing => lowest :: incrimentPassword xs
Just x => x :: xs
Password validity
A password must contain a run of at least 3 incrementing characters, check this
by converting the PasswordChars to their integer representations. Remember
that our Password Vect is backwards compared to the string representation.
incrimentingChars : Vect n PasswordChar -> Bool
incrimentingChars (z :: next@(y :: (x :: xs))) =
let [x, y, z] : Vect _ Int = map (ord . char) [x, y, z]
in if y == x + 1 && z == y + 1
then True
else incrimentingChars next
incrimentingChars _ = False
A password may not contain i, o, or l
noInvalidChars : Vect n PasswordChar -> Bool
noInvalidChars = not . (any (flip contains $ ['i', 'o', 'l'])) . map char
A password contains at least two different non-overlapping pairs.
We check this by pattern matching our password two characters at a time,
consuming both characters if a matched pair is found, and tacking on the Char
the list is composed of to an accumulator list as we go. This list is then
reduced to only its unique elements (it's nub), and checking to see if it's
length is at least 2.
containsPairs : Vect n PasswordChar -> Bool
containsPairs xs = length (nub $ pairs (reverse xs) []) >= 2
where
pairs : Vect m PasswordChar -> (acc : List Char) -> List Char
pairs [] acc = acc
pairs (x :: []) acc = acc
pairs (x :: (y :: xs)) acc =
if x == y
-- If there is a pair, consume it to prevent detecting overlapping pairs
then pairs xs (x.char :: acc)
-- If there isn't a pair, only consume one character
else pairs (y :: xs) acc
Combine our password criteria into one function
passwordCriteria : Vect n PasswordChar -> Bool
passwordCriteria xs = incrimentingChars xs && noInvalidChars xs && containsPairs xs
Find the next password
Find the next password based on a criteria function
findNextPassword :
(f : Vect n PasswordChar -> Bool) -> (password : Vect n PasswordChar)
-> Vect n PasswordChar
findNextPassword f password =
let next = incrimentPassword password
in if f next
then next
else findNextPassword f next
Part Functions
Part 1
part1 : Eff (PartEff String) (String, Password)
part1 = do
input <- map trim $ askAt "input"
password <- parsePassword input
info "Starting password: \{show password} -> \{passwordToString password}"
let next_password = findNextPassword passwordCriteria password
pure (passwordToString next_password, next_password)
Part 2
part2 : Password -> Eff (PartEff String) String
part2 password = do
info
"Second starting password: \{show password} -> \{passwordToString password}"
let next_password = findNextPassword passwordCriteria password
pure $ passwordToString next_password