VictorTaelin

You're a code completion assistant.
###
-- Checker:
-- 
module Kind.Type where

import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M

import Debug.Trace

VictorTaelin

You're a code completion assistant.

###

-- Type.hs:
-- 
module Kind.Type where

import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M

VictorTaelin

You're a code completion assistant.
###
-- 
module Kind.Type where

import qualified Data.IntMap.Strict as IM
import qualified Data.Map.Strict as M

import Debug.Trace
import Data.Word (Word32)

VictorTaelin

Getters and Setters in Kind

The verbosity of nested fields

One of the most annoying aspects of pure functional programming is getting, setting and mutating deeply nested fields. In impure languages like JavaScript, this was never a problem. For example, consider the following object:

VictorTaelin

from: https://discord.com/channels/767397347218423858/767397347218423861/1296580936292499540


Taelin — Today at 5:41 PM
@AndrasKovacs i see you often treat lambda-case and case-of with different constructors. why? is there any obvious cons to just treating (λ{ ... } arg) as a case-of?
Taelin — Today at 6:09 PM
actually, also, consider this:

Main
: ∀(P: ∀(x: B/Bool) *) →

VictorTaelin

I: 1 5 9 3 0 0 A 8 1 E D F 6 5 4 8
O: 1 1 0 6 9 D A 4 5 E 0 5 3 F 8 8

I: 3 0 E C 6 1 F B 3 B 4 F 7 3 E 1
O: 3 3 6 7 E 4 F E 0 B 1 3 C F B 1

I: 8 4 7 C 1 8 7 1 F 0 1 B 9 8 7 6
O: 8 F 1 9 7 1 7 7 4 0 8 8 C B 1 6

I: 3 2 9 D A 2 C 2 D 3 F D 7 F B 6

VictorTaelin

THE PROBLEM

🌲 Invert a binary tree! 🌲

Except with 3 catches:

1. It must invert the keys ("bit-reversal permutation")
2. It must be a dependency-free, pure recursive function
3. It must have type Bit -> Tree -> Tree (i.e., a direct recursion with max 1 bit state)

VictorTaelin

Let an AB symbol be one of 4 possible variants:

  data AB : Set where
    A# : AB
    #A : AB
    B# : AB
    #B : AB

Let an AB Term be a list of AB symbols:

VictorTaelin

// Computes modular exponentiation by repeated ENUM rotation.
// 
// To compute `a ^ b % M`, we:
// - 1. Create a generic ENUM with M variants: enum T { v0, v1, v2, ... vM }
// - 2. Create a generic ENUM rotator: v0 -> v1, v1 -> v2, ... v1 -> v0
// - 3. Apply that rotator a^b times to v0; the result will be `a ^ b % M`!
// 
// To test this, we compute `(123 ^ 10) % 257`.
// This should require at least 792594609605189126649 function calls.
// A Macbook M3 would take about 25,000 years to *count* to that number.

VictorTaelin

<0>(HVM_MAIN_CALL)
----------------
<0>(HVM_MAIN_CALL)
----------------
<0>(Main)
----------------
<0>(Main)
----------------
<0>(Quote (APP (C2a) (C2b)) 0)
----------------