pedrominicz

{
module Lex where
}

%wrapper "basic"

tokens :-
  $white+       ;
  [^ $white]+   { id }

pedrominicz

{
module Lazy where

import Data.ByteString (ByteString)
import qualified Data.ByteString.Lazy as B
}

%wrapper "monadUserState-bytestring"

$alpha = [A-Za-z]

pedrominicz

-- https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
-- http://www.rntz.net/post/2019-01-18-binding-in-agda.html
-- Agda version: https://gist.github.com/pedrominicz/74dfec469ce44ccb88ccf8d04c084727

inductive type : Type
| arrow : type → type → type
| unit : type

def ctx : Type 1 := type → Type

pedrominicz

<!doctype html>
<html>
<head>
  <meta charset="utf-8" />
  <meta http-equiv="content-type" content="text/html; charset=utf-8" />
  <meta name="viewport" content="width=device-width, initial-scale=1" />

  <title>Timer</title>

  <link rel="icon" href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAEAAAABCAYAAAAfFcSJAAAAC0lEQVR4nGNgAAIAAAUAAXpeqz8AAAAASUVORK5CYII=">

pedrominicz

The most important setting

The VSCode binary available on the official website IS NOT FREE SOFTWARE ("free" as in "freedom"). The binary there is under a proprietary license. VSCode's source code is under the MIT license, but the MIT license allows binaries to be redistributed under a proprietary license.

Free distributions of VSCode exist, namely Code OSS and VSCodium. However, Code OSS ships the default VSCode configuration, meaning it comes with telemetry enabled and SENDS USAGE DATA TO MICROSOFT. VSCodium comes with telemetry disabled. Therefore, I recommend using VSCodium.

With that in mind, whatever VSCode distribution you choose, the most important setting in this guide is:

"telemetry.telemetryLevel": "off"

pedrominicz

        .text
        .globl _start
_start:
        mov $1, %rax
        mov $1, %rdi
        mov $hello_world, %rsi
        mov $13, %rdx
        syscall

        mov $60, %rax

pedrominicz

module List where

data List a = Nil | Cons a (List a) deriving (Eq, Show)

instance Functor List where
  fmap f Nil = Nil
  fmap f (Cons a as) = Cons (f a) (fmap f as)

instance Applicative List where
  pure a = Cons a Nil

pedrominicz

{-# LANGUAGE DeriveFunctor #-}

module Reverse where

-- https://tech-blog.capital-match.com/posts/5-the-reverse-state-monad.html

import Control.Monad.State
import qualified Data.Map as M

newtype ReverseState s a = ReverseState { runReverseState :: s -> (a, s) }

pedrominicz

{-# LANGUAGE TupleSections #-}

module Kappa where

-- https://en.wikipedia.org/wiki/Kappa_calculus
-- https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=4854F9750FC1F1D658CC3694052C6A84?doi=10.1.1.53.715&rep=rep1&type=pdf
-- http://www.megacz.com/berkeley/garrows/megacz-pop-talk.pdf

import Control.Monad.Reader
import Safe

pedrominicz

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}