Elvecent

The purpose of this text is to guide a reader through the first step towards grokking continuations as presented in Haskell (callCC not covered). The reader is assumed to have basic knowledge of Haskell including some understanding of monads.

Abstracting away computations

Suppose we are given a list of lists of integers and we want to compute the sum of squares of products of those lists. This task naturally breaks down into three steps:

1. Take product of each list of integers and thus form a new list of integers.
2. In that list, square every integer, again forming a new list of integers.
3. Summate the resulting list.

But to produce this algorithm we need to parse the whole problem and revert it (i. e. start with the last step): the problem's descriptions starts with "sum" and the corresponding algorithm starts with "product". Does it really need to be like this?

Elvecent

module Universal where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open Relation.Binary.PropositionalEquality.≡-Reasoning
open import Agda.Primitive
open import Data.Nat hiding (_⊔_)
open import Data.Unit hiding (setoid)
open import Data.Bool
open import Data.Nat.Properties

Elvecent

data List {α} : Set α → Set α where
  [] : ∀ {X} → List X
  _::_ : ∀ {X} → X → List X → List X

map : ∀ {α β} → {A : Set α} → {B : Set β} →
      (f : A → B) → List A → List B
map f [] = []
map f (x :: xs) = f x :: map f xs

data hList {α} : List (Set α) → Set α where

Elvecent

Module ClassicLogic.
  Definition LEM := forall A : Prop, A \/ ~A.
  Definition CONTRA := forall A B : Prop, (~A -> ~B) -> (B -> A).

  Axiom lem : LEM.
  Axiom contra : CONTRA.

  Notation "( x , y , .. , z )" := (conj .. (conj x y) .. z) (at level 0).
End ClassicLogic.

Elvecent

Require Import Coq.Lists.List.
Import ListNotations.

Inductive hlist : list Type -> Type :=
| nil : hlist []
| cons {Ts : list Type}
       {T : Type} : T -> hlist Ts -> hlist (T :: Ts).

Notation "[ ]" := nil (format "[ ]") : hlist_scope.
Notation "[ x ]" := (cons x nil) : hlist_scope.

Elvecent

{-# Language TypeSynonymInstances
, FlexibleInstances
, MultiParamTypeClasses
, KindSignatures
, GADTs
, DataKinds
, TypeFamilies
, AllowAmbiguousTypes
, TypeApplications
#-}

Elvecent

{-# Language GADTs,
DataKinds,
KindSignatures,
StandaloneDeriving,
DeriveFunctor,
TypeFamilies
#-}

import Data.Function

Elvecent

Minimal Haskell Emacs configuration, from scratch

This little instruction shows how to set up Emacs with some packages to start writing Haskell in a more or less convenient way (including, but not limited to: smart auto completion, type info, autoformatting).

Get emacs

First step: get Emacs for your platform. This should be simple.

Find your init file

That's usually ~/.emacs on unix-like systems. ~ stands for "home folder" and on Windows it's usually AppData\Roaming. Check this out.

Set up MELPA

Elvecent

import 'package:flutter/material.dart';
import 'func.dart';

class Message {
  Message(this.text, this.isMe);

  String text;
  bool isMe;
}

Elvecent

{-# Language DeriveFunctor #-}

module Parser where

newtype Parser a = Parser { parse :: String -> [(a, String)] }
  deriving Functor

parserBind :: Parser a -> (a -> Parser b) -> Parser b
parserBind (Parser p) mf = Parser $ \s ->
  p s >>= (\(x,s) -> parse (mf x) s)