VictorTaelin

// This is an example implementation of the Calculus of Constructions, using first
// class Anns that compute, inspired by Interaction Type Theory. This allows us to
// completely get rid of contexts, and the checker function becomes minimal, as
// it just needs to collapse chained ANNs into equalities. The code below is an
// initial demo of such idea (very new, not tested).

type List<A> =
  | { tag: "Cons"; head: A; tail: List<A> }
  | { tag: "Nil"; };

VictorTaelin

study: https://link.springer.com/article/10.1007/s11357-023-00980-6

Q: What are the main findings of the article above?

A: The main findings of the article are that a plasma fraction treatment derived from young adult pigs, termed E5, significantly reversed aging in rats according to epigenetic clocks and other biomarkers of aging. The treatment more than halved the epigenetic ages of blood, heart, and liver tissue, and also showed a significant rejuvenation effect in the hypothalamus. Alongside this, the treatment led to improvements in organ function, reduced markers of chronic inflammation and oxidative stress, increased antioxidant levels, and improved cognitive functions in the rats. The study also developed six different epigenetic clocks for rat tissues, two of which can be applied to humans as well.

Q: How clinically significant were the objective improvements observed? Provide an extensive list of measured markers and effect size.

A: The objective improvements observed in the study were clinicall

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