Idris 2

• Based on Quantitative Type Theory (QTT)
  • Theory worked on by McBride, Atkey, et al

General

• Packages: https://idris2.readthedocs.io/en/latest/tutorial/packages.html
• Namespaces: https://idris2.readthedocs.io/en/latest/tutorial/modules.html#explicit-namespaces
  • Mutliple definitions with same name can be present in the same module, but in different namespaces.
• total: declare that a function is total
• mutual: for declaring mutually recursive types
• Anonymous functions. Like
  • \x => x
  • \x : Int => x
• 'Docstrings': Each line starts with |||
  • https://docs.idris-lang.org/en/latest/reference/documenting.html
• Search based on types of definitions: https://docs.idris-lang.org/en/latest/reference/type-directed-search.html

Implicit arguments

From here:

names which begin with a lower case letter are automatically bound as implicit arguments in types

Dependent pairs

https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#dependent-pairs

• Two values. First value can show up in the second.
• aka Sigma types

Eg: an implementation of Vector:

(n:Nat ** Vector n Int)

Another example??ˡ: (n : Nat) * (vars : Vect n String) * ScopedLC vars)

Multiplicty

• Every variable has a multiplicty associated with it.
• Courtesy of Quantitative Type theory (QTT) on which idris2 is based.
• A concept apparently not there in idris1??

Values:

• 0: Erased at runtime
• 1: Used exactly once at runtime
• Unrestricted: Can be used any number of times at runtime

Explicit multiplicity examples:

• (0 n: Nat)
• (1 n: Nat)

Default multiplicity values:

• No multiplicity annotation => unrestricted
• Implicit argument => 0

Fun fact: Following is a function that cannot be realized as it requires two instances of a but only 1 is allowed:

• duplicate : (1 x:a) -> (a, a)

https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html

REPL

https://docs.idris-lang.org/en/latest/reference/repl.html

• :?: show help
• :import / :module: import modules / packages
• :t: show type of a value
• :ti: show type (including implicit arguments) of a value

λΠ> :doc **
Used to build dependent pairs together with parentheses

$ rlwrap idris2 -p contrib

λΠ> :import Data.Telescope.Telescope
Imported module Data.Telescope.Telescope

vim plugin: idir

• Plugin seems not so maintained: https://github.com/edwinb/idris2-vim
• This is for idris1 apparently: https://github.com/idris-hackers/idris-vim

Book: Type driven development with Idirs

• Uses idris 1.
• https://www.manning.com/books/type-driven-development-with-idris

Idris1 vs Idris2

• No separate tactics??
• Type: Type problem still not fixed in idris2 ??
• Idris 2 is bootstrapping.
• Idris 2 is way faster.

Category

• An interface

• Part of idris2 standard library

• https://www.idris-lang.org/docs/idris2/0.6.0/contrib_docs/docs/Control.Category.html

• (.): compose arrows

  • cat b c -> cat a b -> cat a c

• (>>>): compose with arg order changed ('flow')

  • cat a b -> cat b c -> cat a c

Morphisms

• A record type
• https://www.idris-lang.org/docs/idris2/0.6.0/base_docs/docs/Data.Morphisms.html
• Looks like it's essentially a wrapper for a function type.

record Morphism : Type -> Type -> Type
  Mor : (a -> b) -> Morphism a b

Kleislimorphism

https://www.idris-lang.org/docs/idris2/0.6.0/base_docs/docs/Data.Morphisms.html#Data.Morphisms.Kleislimorphism

• Normal morphism: a -> b
• Kleisli morphism: Monad m => a -> m b

—

--                    a -> m b        a       b
--                       |            |       |  
--                +------+-----+   +--+-+  +--+-+
--                |            |   |    |  |    |
Kleislimorphism : (Type -> Type) -> Type -> Type -> Type

• Constructor: Kleisli : (a -> m b) -> Kleislimorphism a b

Contravariant functors

https://www.idris-lang.org/docs/idris2/0.6.0/base_docs/docs/Data.Contravariant.html#Data.Contravariant.Contravariant

instance Contravariant : (Type -> Type) -> Type
    -- Same as `(>$<)`
    contramap : (a -> b) -> f b -> f a
    (>$) : 

Telescope

• 'Variable context in a dependently typed program'
• Three kinds in the contrib package of idris2
  • A 'left-nested' sequence of deptype
  • A 'right-nested' sequence of deptype
  • A tree-shaped sequence of deptype

λΠ> :t Telescope
Data.Telescope.Telescope.Left.Telescope : Nat -> Type
Data.Telescope.Telescope.Right.Telescope : Nat -> Type
Data.Telescope.Telescope.Tree.Telescope : Nat -> Type

—

-- Left-nested
-- New values are appended. ie, nesting happens on the left.
--
namespace Left
  data Telescope : Nat -> Type
    Nil : Telescope 0
    (-.) : (gamma : Telescope k) -> TypeIn gamma -> Telescope (S k)

--------------------

-- Right-nested
-- New values are prepended. ie, nesting happens on the right.
--
namespace Right
  data Telescope : Nat -> Type
    Nil : Telescope 0
    (.-) : (ty : Type) -> (ty -> Telescope k) -> Telescope (S k)

--------------------

-- Tree-shaped
--
namespace Tree
  data Telescope : Nat -> Type
    Nil : Telescope 0
    Elt : Type -> Telescope 1
    (++) : (gamma : Telescope m) -> (Environment gamma -> Telescope n) -> Telescope (m + n)

See:

• https://www.idris-lang.org/docs/idris2/0.6.0/contrib_docs/docs/Data.Telescope.html
• https://www.idris-lang.org/docs/idris2/0.6.0/contrib_docs/docs/Data.Telescope.Telescope.html

—

• TypeIn : Telescope k -> Type: A type with dependencies in the context represented by the telescope

Misc

• Katla: Tool to convert idris code to latex or html
  • https://github.com/idris-community/katla
• idris2doc: generate documentation for idris as html ??

Trivia

• Etymology: Name of a dragon in a story.