gelisam

-- A proof of concept for a value-based debugging technique: instead of
-- debugging by imperatively stepping through the evaluation, we instead
-- produce a value representing the evaluation tree.
--
-- This value can then be manipulated like any other value, e.g. instead adding
-- a breakpoint and stepping until the breakpoint is hit, you can write an
-- ordinary function which recurs into the evaluation tree until it finds a node
-- of interest. This way, more complex conditions can be easily expressed, e.g.
-- "find the smallest subtree in which a call of 'double' does not result in an
-- output which is the double of its input".

o11c

Note: this was originally several Reddit posts, chained and linked. But now that Reddit is dying I've finally moved them out. Sorry about the mess.

---

URL: https://www.reddit.com/r/ProgrammingLanguages/comments/up206c/stack_machines_for_compilers/i8ikupw/ Summary: stack-based vs register-based in general.

There are a wide variety of machines that can be described as "stack-based" or "register-based", but not all of them are practical. And there are a lot of other decisions that affect that practicality (do variables have names or only address/indexes? fixed-width or variable-width instructions? are you interpreting the bytecode (and if so, are you using machine stack frames?) or turning it into machine code? how many registers are there, and how many are special? how do you represent multiple types of variable? how many scopes are there(various kinds of global, local, member, ...)? how much effort/complexity can you afford to put into your machine? etc.)

• a pure stack VM can only access the top elemen

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.

LSLeary

module Cube where

import Data.Functor.Const (Const(..))
import Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))


type (&&) = Product
type (||) = Sum

typeswitch-dev

bits 64
org 0x4000000

elf_header:
.size       equ .end - $
.e_ident    db 0x7F, 'E', 'L', 'F'  ; EI_MAG0 ... EI_MAG3
            db 2                    ; EI_CLASS: 1 => 32 bits, 2 => 64 bits
            db 1                    ; EI_DATA: 1 => lil endian, 2 => big "
            db 1                    ; EI_VERSION: original version
            db 0                    ; EI_OSABI: 0 => System V ABI

typeswitch-dev

org 0 ; We use "org 0" so Relative Virtual Addresses (RVAs) are easy.
      ; This means that when we want an absolute Virtual Address we have
      ; to add IMAGE_BASE to the RVA (or whatever the base of that section is)

IMAGE_BASE equ 0x400000
SECT_ALIGN equ 0x200
FILE_ALIGN equ 0x200

msdos_header:
.magic      db 'MZ'

typeswitch-dev

bits 64
org 0x1000

mach_header:
.magic      dd 0xFEEDFACF       ; MH_MAGIC_64
.cputype    dd 0x01000007       ; CPU_ARCH_ABI64 | CPU_TYPE_I386
.cpusubtype dd 0x00000003       ; CPU_SUBTYPE_LIB64 | CPU_SUBTYPE_I386_ALL
.filetype   dd 0x2              ; MH_EXECUTE
.ncmds      dd 3
.sizeofcmds dd mach_cmds_end - mach_cmds_start

Gabriella439

The inference judgment is:

Γ ⊢ e ⇒ A ⊢ Δ

… where:

• Γ (an input) is a context which is a map from variables to their types
• e (an input) is an expression whose type we wish to infer
• A (an output) is the inferred type
• Δ (an output) is a context which is a map from variables to their types

Trebor-Huang

{-# OPTIONS --prop --without-K --safe #-}

module Synthesis where

-- Utilities
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Nat using (zero; suc; _+_) renaming (Nat to ℕ)

infixl 8 _∧_ _×_

lukaszlew

-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
import Data.List (delete, union)
{- HLINT ignore "Eta reduce" -}

-- File mnemonics:
--   env = typing environment
--   vid = variable identifier in Bind or Var
--   br = binder variant (Lambda or Pi)
--   xyzTyp = type of xyz
--   body = body of Lambda or Pi abstraction