Brandon Elam Barker bbarker
bbarker
/ unison-witness.nu
Last active
October 29, 2026 19:06
Check a Unison type witness's typeLinks against its constructors' indices, and a hand-kept list of a GADT's constructors, through ucm transcript.fork
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/env nu | |
| # Checks a Unison type witness against the function that links its types, | |
| # and optionally a hand-kept list of a GADT's constructors against the GADT. | |
| # | |
| # A witness is a GADT with one constructor per type, each fixing its index: | |
| # | |
| # type Stored a where | |
| # SubmissionS : Stored Submission | |
| # AccountS : Stored Account |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Arcane | |
| # Generated with deterministic seed 0x31ae2d279086ccff derived from ISRC USUAN1100831. | |
| # Base presets sourced from video/presets.csv for USUAN1100831. | |
| # Selection: smooth route through 7 anchors drawn from 24 sampled configurations. | |
| # Durations are snapped to downbeats at 92.2 bpm (confidence 0.48); 4 of 26 land on a section change. | |
| # @ 00:00.000 downbeat 92.2 bpm | Start anchor: sampled 1 | |
| "--flame symmetric --wave rings --border clear --palette longs --table 3 --translate smoke --display cylinder --environment palettehaze --particles embers --aura echoshell", 12.910, 1 | |
| # @ 00:12.910 downbeat 92.2 bpm | |
| "--flame symmetric --wave rings --border clear --palette fadern4 --table 3 --translate smoke --display cylinder --environment palettehaze --particles embers --aura echoshell", 12.887, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Aretes | |
| # Generated with deterministic seed 0x7f3a2a27bc5545d7 derived from ISRC USUAN1100325. | |
| # Base presets sourced from video/presets.csv for USUAN1100325. | |
| # Selection: smooth route through 6 anchors drawn from 24 sampled configurations. | |
| # Durations are sampled from 12-15 seconds. | |
| # Start anchor: sampled 14 | |
| "--flame water --wave walk --border clear --palette troll --table 9 --translate smoke --display sphere --environment palettehaze --particles flow --aura off", 12, 1 | |
| "--flame water --wave wire --border clear --palette troll --table 9 --translate smoke --display sphere --environment palettehaze --particles flow --aura off", 13, 1 | |
| "--flame water --wave wire --border clear --palette nice --table 9 --translate smoke --display sphere --environment palettehaze --particles flow --aura off", 15, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Apero Hour | |
| # Generated with deterministic seed 0xb7b25286261fd4f6 derived from ISRC USUAN1700070. | |
| # Base presets sourced from video/presets.csv for USUAN1700070. | |
| # Selection: smooth route through 6 anchors drawn from 24 sampled configurations. | |
| # Durations are snapped to downbeats at 69.8 bpm (confidence 0.71); 4 of 22 land on a section change. | |
| # @ 00:00.000 downbeat 69.8 bpm | Start anchor: sampled 23 | |
| "--flame water --wave hline --border clear --palette indigo --table 3 --translate ripple --display plane --environment palettehaze --particles flow --aura echoshell", 14.257, 1 | |
| # @ 00:14.257 downbeat 69.8 bpm | |
| "--flame symmetric --wave hline --border clear --palette indigo --table 3 --translate ripple --display plane --environment palettehaze --particles flow --aura echoshell", 13.723, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Angevin | |
| # Generated with deterministic seed 0x947a72e39e4e0076 derived from ISRC USUAN1200110. | |
| # Base presets sourced from video/presets.csv for USUAN1200110. | |
| # Selection: smooth route through 6 anchors drawn from 24 sampled configurations. | |
| # Durations are snapped to downbeats at 70.0 bpm (confidence 0.39); 2 of 21 land on a section change. | |
| # @ 00:00.000 downbeat 70.0 bpm | Start anchor: sampled 11 | |
| "--flame fade --wave fall --border wave --palette med --table 7 --translate smoke --display cylinder --environment volumetricnebula --particles off --aura off", 14.141, 1 | |
| # @ 00:14.141 downbeat 70.0 bpm | |
| "--flame fade --wave fall --border wave --palette med --table 7 --translate smoke --display cylinder --environment black --particles off --aura off", 13.723, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Ancient Winds | |
| # Generated with deterministic seed 0x9c94b84dee85cf96 derived from ISRC USUAN1900043. | |
| # Base presets sourced from video/presets.csv for USUAN1900043. | |
| # Selection: smooth route through 66 anchors drawn from 24 sampled configurations. | |
| # Durations are sampled from 12-15 seconds. | |
| # Start anchor: sampled 22 | |
| "--flame down-subtle --wave fall --border clear --palette rgb --table 8 --translate smoke --display cylinder --environment volumetricnebula --particles off --aura off", 13, 1 | |
| "--flame fade --wave fall --border clear --palette rgb --table 8 --translate smoke --display cylinder --environment volumetricnebula --particles off --aura off", 14, 1 | |
| "--flame fade --wave fall --border clear --palette volcano7 --table 8 --translate smoke --display cylinder --environment volumetricnebula --particles off --aura off", 14, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Ancient Mystery Waltz (Vivace) | |
| # Generated with deterministic seed 0xd0867f7f5b3a5b00 derived from ISRC USUAN2100006. | |
| # Base presets sourced from video/presets.csv for USUAN2100006. | |
| # Selection: smooth route through 4 anchors drawn from 24 sampled configurations. | |
| # Durations are snapped to downbeats at 136.0 bpm (confidence 0.56); 8 of 20 land on a section change. | |
| # @ 00:00.000 downbeat 136.0 bpm | Start anchor: sampled 1 | |
| "--flame water --wave vline --border amp --palette froth3 --table 9 --translate none --display plane --environment volumetricnebula --particles embers --aura off", 12.887, 1 | |
| # @ 00:12.887 downbeat 136.0 bpm | |
| "--flame water --wave vline --border wave --palette froth3 --table 9 --translate none --display plane --environment volumetricnebula --particles embers --aura off", 12.446, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Ancient Mystery Waltz (Allegro) | |
| # Generated with deterministic seed 0xd086827f5b3a6019 derived from ISRC USUAN2100005. | |
| # Base presets sourced from video/presets.csv for USUAN2100005. | |
| # Selection: smooth route through 7 anchors drawn from 41 of 72 presets on-mood. | |
| # Durations are snapped to downbeats at 112.2 bpm (confidence 0.66); 8 of 25 land on a section change. | |
| # @ 00:00.000 downbeat 112.2 bpm | Start anchor: dualplane-skyline-hline-metal-table0 | |
| "--flame skyline --wave hline --border clear --palette metal --table 0 --translate none --display dualplane --environment black --particles off --aura off --aura-size 100 --environment-intensity 400 --environment-speed 100 --particle-speed 100", 13.259, 1 | |
| # @ 00:13.259 downbeat 112.2 bpm | |
| "--flame skyline --wave hline --border clear --palette metal --table 7 --translate none --display dualplane --environment black --particles off --aura off --aura-size 100 --environment-intensity 400 --environment-speed 100 --particle-speed 100", 12.748, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Ambiment | |
| # Generated with deterministic seed 0x65b4a627ae024ff2 derived from ISRC USUAN1100630. | |
| # Base presets sourced from video/presets.csv for USUAN1100630. | |
| # Selection: smooth route through 27 anchors drawn from 28 of 72 presets on-mood. | |
| # Durations are sampled from 12-15 seconds. | |
| # Start anchor: cylinder-skyline-rings-fadern4-table0 | |
| "--flame skyline --wave rings --border wave --palette fadern4 --table 0 --translate none --display cylinder --environment palettehaze --particles drift --aura off", 13, 1 | |
| "--flame skyline --wave rings --border wave --palette fadern4 --table 0 --translate none --display screen --environment palettehaze --particles drift --aura off", 14, 1 | |
| "--flame skyline --wave rings --border clear --palette fadern4 --table 0 --translate none --display screen --environment palettehaze --particles drift --aura off", 12, 1 |
We can make this file beautiful and searchable if this error is corrected: It looks like row 7 should actually have 1 column, instead of 3 in line 6.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # ShoggothOx Playlist: Almost in F | |
| # Generated with deterministic seed 0x7f292b27bc46d457 derived from ISRC USUAN1100394. | |
| # Base presets sourced from video/presets.csv for USUAN1100394. | |
| # Selection: smooth route through 38 anchors drawn from 19 of 49 presets on-mood. | |
| # Durations are sampled from 12-15 seconds. | |
| # Start anchor: cones-down-subtle-hline-necklace-table5 | |
| "--flame down-subtle --wave hline --border clear --palette necklace --table 5 --translate none --display cones --environment palettehaze --particles drift --aura off", 15, 1 | |
| "--flame water --wave hline --border clear --palette necklace --table 5 --translate none --display cones --environment palettehaze --particles drift --aura off", 15, 1 | |
| "--flame water --wave hline --border clear --palette necklace --table 5 --translate none --display twisted --environment palettehaze --particles drift --aura off", 14, 1 |
NewerOlder