module Syntax.Basic.Typeclass.Special.Coercible where

import Prelude
import Prim.Coerce (class Coercible)
import Safe.Coerce (coerce)

-- ## Linking to the paper for an (optional) detailed explanation

-- In this file, we'll provide a beginner-friendly summary of the paper
-- that is linked below. For our purposes, we will only explain the bare
-- minimum necessary to make the rest of this file make sense.

-- If you wish to know more, read the paper below. However, be warned that
-- those who are new to functional programming will likely not understand
-- as much until they understand the `Functor` and/or `Foldable` type classes.
-- These are covered in the `Hello World/Prelude-ish` folder in this project.

-- Here's the paper: "Safe zero-cost coercions for Haskell"
-- https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1010&context=compsci_pubs


-- ## Summary of the Problem

-- While we have stated earlier that newtypes are "zero-cost abstractions"
-- in that one does not incur a performance penalty for wrapping and unwrapping
-- a newtyped value, there are some situations where this is not true.

-- For example, let's say you had the following types:

-- | A comment that has multiple lines of text.
newtype MultiLineComment = MultiLineComment String

-- | A comment that has only 1 line of text.
newtype SingleLineComment = SingleLineComment String

-- Let's say we wish to convert an `Array MultiLineComment` into
-- `Array SingleLineComment` via the function,
--     `exposeLines :: String -> Array String`

-- While newtypes are "zero-cost abstractions," this particular algorithm
-- would incur a heavy performance cost. Here's what we would have to do:
-- 1. Convert the `MultiLineComment` type into the `String` type
--      by iterating through the entire `Array MultiLineComment` and unwrapping
--      the `MultiLineComment` newtype wrapper.
-- 2. Use `exposeLines` to convert each multi-line `String` into an `Array`
--      of Strings by iterating through the resulting array.
--      Each `String` in the resulting array would have only 1 line of content.
-- 3. Combine all `Arrays` of single-line `String`s into one Array.
--      In other words, `combine :: Array (Array String) -> Array String`
-- 4. Convert the `String` type into the `SingleLineComment` type
--       by iterating through the final `Array` and wrapping each `String` in a
--      `SingleLineComment` newtype.

-- Steps 1 and 4 are necessary to satisfy type safety. At the type-level,
-- a `String` is not a `MultiLineComment`, nor a `SingleLineComment`.
-- However, those three types do have the same runtime representation. Thus,
-- Steps 1 and 4 are an unnecessary performance cost. Due to using newtypes
-- in this situation, we iterate through the array two times more than needed.

-- A `MultiLineComment` can be converted into a `String` safely and
-- a `String` into a `SingleLineComment` safely. This type conversion
-- process is safe and therefore unnecessary. The problem is that the developer
-- does not have a way to provide the compiler with a proof of this safety.
-- If the compiler had this proof, it could verify it and no longer complain
-- when the developer converts the `Array MultiLineComment` into an
-- `Array String` through a O(1) functio.

-- The solution lays in two parts: the `Coercible` type class
-- and "role annotations."

-- ## Coercible

-- This is the exact definition of the `Coercible` type class. However,
-- we add the "_" suffix to distinguish this fake one from the real one.
class Coercible_ a b where
  coerce_ :: a -> b

-- The `Coercible` type class says, "I can safely convert a value of type `a`
-- into a value of type `b`." This solves our immediate problem, but it
-- introduces a new problem. Since the main usage of `Coercible` is to
-- remove the performance cost of newtypes in specific situations, how do
-- make it impossible to write `Coercible` instances for invalid types?

-- For example, a `DataBox` is a literal box at runtime because it uses the
-- `data` keyword. It actually has to wrap and unwrap the underying value:
data DataBox a = DataBox a

-- The `NewtypedBox` below is NOT a literal box at runtime because
-- it doesn't actually wrap/unwrap the underlying value.
newtype NewtypedBox theValue = NewtypedBox theValue

-- Thus, while we could have a type class instance for `MultiLineComment`,
-- `String`, and `SingleLineComment`, should we have an instance
-- between `DataBox` and `NewtypedBox`? The answer is no.
-- However, how would we tell that to the compiler, so it could verify that
-- for us? The answer is "role annotations."

-- ## Role Annotations

-- For another short explanation, see the answer to the post,
-- "What is a role?" https://discourse.purescript.org/t/what-is-a-role/2109/2

-- Role annotations tell the compiler what rules to follow when determining
-- whether a Coercible instance between two types is valid. There are
-- three possible values: representational, phantom, and nominal.

-- Role annotation syntax follows this syntax pattern:
-- `type role TheAnnotatedType oneRoleAnnotationForEachTypeParameter`

-- ### Representational

-- Representational says,
--  "If `A` can be safely coerced to `B` and the runtime representation of
--     `Box a` does NOT depend on `a`, then `Box a` can be safely
--     coerced to `Box b`." (in contrast to `nominal`)

-- Given a type like Box, which only has one type parameter, `a`...
data Box a = Box a

-- ... we would write the following:
type role Box representational

-- Here's another example that shows what to do when we have
-- multiple type parameters
data BoxOfThreeValues a b c = BoxOfThreeValues a b c
type role BoxOfThreeValues representational representational representational

-- ### Phantom

-- Phantom says,
-- "Two phantom types never have a runtime representation. Therefore,
-- two phantom types can always be coerced to one another."

-- Given a box-like type that has a phantom type parameter, `phantomType`...
data PhantomBox :: Type -> Type
data PhantomBox phantomType = PhantomBox

-- ... we would write the following:
type role PhantomBox phantom

-- Here's another example that mixes role annotations:
data BoxOfTwoWithPhantom :: Type -> Type -> Type -> Type
data BoxOfTwoWithPhantom a phantom b = BoxOfTwoWithPhantom

type role BoxOfTwoWithPhantom representational phantom representational

-- ### Nominal

-- Nominal says,
--  "If `A` can be safely coerced to `B` and the runtime representation of
--     `Box a` DOES depend on `a`, then `Box a` can NOT be safely
--     coerced to `Box b`." (in contrast to `representational`)

-- When we don't have enough information (e.g. writing FFI), we default
-- to the nominal role annotation. Below, we'll see why.

-- For example, let's consider `HashMap key value`. Let's say we use a type class
-- called `Hashable` to calculate the hash of a given key. Since newtypes
-- can implement a different type class instance for the same runtime
-- representation, wrapping that value in a newtype and then hashing it
-- might not produce the same hash as the original. Thus, we would return
-- a different value.

class Hashable key where
  hash :: key -> Int

instance hashableInt :: Hashable Int where
  hash key = key

newtype SpecialInt = SpecialInt Int
derive instance eqSpecialInt :: Eq SpecialInt
instance hashableSpecialInt :: Hashable SpecialInt where
  hash (SpecialInt key) = key * 31

data Map key value = Map key value

type role Map representational representational

data Maybe a = Nothing | Just a
derive instance eqMaybe :: (Eq a) => Eq (Maybe a)

lookup :: forall key1 key2 value
        . Coercible key2 key1 => Hashable key1
       => Map key1 value -> key2 -> Maybe value
lookup (Map k value) key =
    coercedKey :: key1
    coercedKey = coerce key
  in if hash k == hash coercedKey
       then Just value
       else Nothing

normalMap :: Map Int Int
normalMap = Map 4 28

-- This will output `true`
testLookupNormal :: Boolean
testLookupNormal = (lookup normalMap 4) == (Just 4)

-- This will output `false`
testLookupSpecial :: Boolean
testLookupSpecial = (lookup specialMap 4) == (Just 4)
    -- changes `Map 4 28` to `Map (SpecialInt 4) 28`
    specialMap :: Map SpecialInt Int
    specialMap = coerce normalMap

-- To prevent this possibility from ever occurring, we indicate that
-- a type parameter's role is 'nominal'. Rewriting our `Map` implementation
-- so that `key` is nominal would prevent this from occurring. Since
-- the `value` type parameter does not affect the runtime representation,
-- it can be representational.

data SafeMap key value = SafeMap key value

type role SafeMap nominal representational