witt3rd

Pluto.jl

Watch this

Setup

Get Julia

macOS

witt3rd

### A Pluto.jl notebook ###
# v0.12.3

using Markdown
using InteractiveUtils

# This Pluto notebook uses @bind for interactivity. When running this notebook outside of Pluto, the following 'mock version' of @bind gives bound variables a default value (instead of an error).
macro bind(def, element)
    quote
        local el = $(esc(element))

witt3rd

data Foo a = Bar a
           | Baz (Foo a) (Foo a)

fooEq : DecEq a => a -> a -> Foo a -> Foo a -> Maybe (Foo a)
fooEq x y f g = case decEq x y of
  Yes _ => Just (Baz f g)
  No  _ => Nothing

comb : DecEq a => Foo a -> Foo a -> Maybe (Foo a)
comb f@(Bar x  ) g@(Bar y  ) = fooEq x y f g -- < ok

witt3rd

Z Notation (zed)

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{zed-csp}
\usepackage{amsthm}

\theoremstyle{definition}

witt3rd

data Foo : (x : List a) -> (y : List b) -> Type where
  MkFoo : (bar: a -> b) -> Foo x y

bar : Foo {a} {b} x y -> a -> b
bar (MkFoo _) x' = ?rhs

{-
  b : Type
  a : Type
  y : List b

witt3rd

record Foo where
  constructor MkFoo
  from : Type
  to : Type

bar : (a : Foo) -> (x : from a) -> (to a)
-- impl not important

baz : (a : Foo) -> (b : Foo) -> ((to b) = (from a)) => (x: from b) -> (to a)

witt3rd

module RandomDouble

import Data.Bits
import Data.Vect
import Effects
import Effect.StdIO
import Effect.Random

-- 2^53 as an Integer
twoTo53 : Integer

witt3rd

Idris Cookbook

From Haskell

newtype

newtype WorldM a = WorldM { asT :: WorldT a }

witt3rd

nix

Install

macOS

Follow the recommended approach to prepare for the standard Linux install (below).

Linux / WSL

witt3rd

Type-Driven Development with Idris: Reading Group Questions and Challenges

Chapter 3. Interactive development with types

• Functions in Idris are defined by collections of pattern-matching equations.
• Patterns arise from the constructors of a data type.

1. Describe "type declaration", "type definition", "equation", "expression"
2. Are type declarations required? When (not)?
3. What is referential transparency?
4. Can pattern matching match a specific value?