VictorTaelin

ported from https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda

JS

const Lam = bod => lam => app => vah => lam(bod);
const App = fun => arg => lam => app => vah => app(fun)(arg);
const Var = exp => lam => app => vah => vah(exp);

const nz = v => nz => ns => nz(v);

VictorTaelin

data Complex = C Double Double deriving Show
data Nat     = E | O Nat | I Nat deriving Show
data Tree a  = L a | B (Tree a) (Tree a) deriving Show

cScale :: Double -> Complex -> Complex
cScale s (C ar ai) = C (ar * s) (ai * s)

cAdd :: Complex -> Complex -> Complex
cAdd (C ar ai) (C br bi) = C (ar + br) (ai + bi)

VictorTaelin

Implementing complex numbers and FFT with just datatypes (no floats)

In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats.

VictorTaelin

import Debug.Trace
import Data.Bits

-- FFT Algorithm
-- =============

data Nat    = E | O Nat | I Nat
data Tree a = L a | B (Tree a) (Tree a)
type GN     = Tree Int

VictorTaelin

data Complex = C Double Double deriving Show

cScale :: Double -> Complex -> Complex
cScale s (C ar ai) = C (ar * s) (ai * s)

cAdd :: Complex -> Complex -> Complex
cAdd (C ar ai) (C br bi) = C (ar + br) (ai + bi)

cSub :: Complex -> Complex -> Complex
cSub (C ar ai) (C br bi) = C (ar - br) (ai - bi)

VictorTaelin

(Rot (V z))   = (V (- 0.0 z))
(Rot (G x y)) = (G (Rot y) x)

(Add (V z)   (V w))   = (V (+ z w))
(Add (G x y) (G w z)) = (G (Add x w) (Add y z))

(Get (V x)   f) = (f x)
(Get (G x y) f) = (f x y)

Nil     = λm λx (m x)

VictorTaelin

Flip (n: Nat) : Nat
Flip Nat.zero            = 1n
Flip (Nat.succ Nat.zero) = 0n

Mod2 (n: Nat) : Nat
Mod2 Nat.zero     = Nat.zero
Mod2 (Nat.succ n) = Flip (Mod2 n)

IsEven (n: Nat) : Type
IsEven Nat.zero                = Unit

VictorTaelin

#IfWinActive, LDPlayer
~RButton::
{
    MouseGetPos, origX, origY ; Save original mouse position
    SysGet, monitor, MonitorWorkArea ; Get monitor dimensions

    centerX := monitorRight // 2 ; Calculate the center of the screen (X-axis)
    centerY := monitorBottom // 2 ; Calculate the center of the screen (Y-axis)

    ; Calculate the new position with 50% of the distance from the center of the screen

VictorTaelin

Notes on this tweet.

• The screenshots were taken on different sessions.

• The entire sessions are included on the screenshots.

• I lost the original prompts, so I had to reconstruct them, and still managed to reproduce.

• The "compressed" version is actually longer! Emojis and abbreviations use more tokens than common words.

VictorTaelin

//// Aplicar Scott = Pattern Match
//(n
  //// case succ
  //λpred(...)
  //// case zero
  //case_zero
//)

//// Aplicar Church = Fold Recursivo