• Implementation Alternatives
• How Strings Currently Work
• Alternative 1: Defining Unicode Strings in Idris, on top of Bytestrings
• Alternative 2: Adding a Built-In Unicode String Type
• Literals
• Built-in Types
• Primitive Functions
• Foreign Function Interface
• Functions in the Prelude
• Internal Representation of Unicode Strings
• Additional Ideas (aka Future Work)
• Related Work
• Appendix: String Encodings
• UTF-8
• UTF-16
• UTF-32 / UCS-4
• Mixed Encodings
• Appendix: References