TypeHoles
@typeholes.bsky.social
Interested in all things programming, cooking, cats.
Love to explore new programming languages and build dev tools.
Love to explore new programming languages and build dev tools.
TFW when you hit the documentation and where the documentation should be is two links to video tutorials :(
October 8, 2025 at 11:05 PM
TFW when you hit the documentation and where the documentation should be is two links to video tutorials :(
The photos app just showed me this. Coincidence or has the algorithm picked up some mean spirited sarcasm
July 22, 2025 at 12:33 AM
The photos app just showed me this. Coincidence or has the algorithm picked up some mean spirited sarcasm
What I want from AI is good function names given a type signature or definition. For example, what do I call:
def hmm (f: b -> c -> d) (g: a -> b) (h: a -> c) (i: a) := f (g i) (h i)
I know what it does and when I need it, but no name seems right.
def hmm (f: b -> c -> d) (g: a -> b) (h: a -> c) (i: a) := f (g i) (h i)
I know what it does and when I need it, but no name seems right.
July 20, 2025 at 2:32 AM
What I want from AI is good function names given a type signature or definition. For example, what do I call:
def hmm (f: b -> c -> d) (g: a -> b) (h: a -> c) (i: a) := f (g i) (h i)
I know what it does and when I need it, but no name seems right.
def hmm (f: b -> c -> d) (g: a -> b) (h: a -> c) (i: a) := f (g i) (h i)
I know what it does and when I need it, but no name seems right.
Meeting new people today, so kicking it up a bit.
July 11, 2025 at 7:46 PM
Meeting new people today, so kicking it up a bit.
I feel like I spent the night as a human pinata and my hair is a different color now, so yeah best concert yet. 10/10 would do again (after a recovery period cause I'm too old for this much fun)
July 5, 2025 at 1:45 PM
I feel like I spent the night as a human pinata and my hair is a different color now, so yeah best concert yet. 10/10 would do again (after a recovery period cause I'm too old for this much fun)
Totally wiped after this week, but I'm not going to relax without doing something creative so I started whatever this is.
SVGs are kind of annoying
SVGs are kind of annoying
June 29, 2025 at 4:11 AM
Totally wiped after this week, but I'm not going to relax without doing something creative so I started whatever this is.
SVGs are kind of annoying
SVGs are kind of annoying
Nothing better than coming home from a walk to find the kids jamming together
June 27, 2025 at 1:29 AM
Nothing better than coming home from a walk to find the kids jamming together
Outdoor shows in Florida can be rough. Playing between bouts of rain. On the plus side, you sometimes get cool mermaids
May 11, 2025 at 12:38 AM
Outdoor shows in Florida can be rough. Playing between bouts of rain. On the plus side, you sometimes get cool mermaids
Is there any CS topic as poorly explained, widely misunderstood, and prevalently misapplied as relational database theory?
May 8, 2025 at 9:40 PM
Is there any CS topic as poorly explained, widely misunderstood, and prevalently misapplied as relational database theory?
My kid (bass) said their new band was a little harder. I was not prepared for this. Incredible.
May 5, 2025 at 12:06 AM
My kid (bass) said their new band was a little harder. I was not prepared for this. Incredible.
Oh heck, Face the Fence is gonna make me take off my glasses and act the fool
May 4, 2025 at 9:48 PM
Oh heck, Face the Fence is gonna make me take off my glasses and act the fool
Grim Gardener making Jewish I could still sport long hair without looking utterly ridiculous
May 4, 2025 at 9:15 PM
Grim Gardener making Jewish I could still sport long hair without looking utterly ridiculous
Iron Curtain live at the Crow Bar in Ybor
May 4, 2025 at 8:11 PM
Iron Curtain live at the Crow Bar in Ybor
Roast pork with a whisky cilantro cream sauce. I'll let you decide whether the plating is a skill issue or intentionally satirical.
May 4, 2025 at 12:01 AM
Roast pork with a whisky cilantro cream sauce. I'll let you decide whether the plating is a skill issue or intentionally satirical.
Why do I love bluesky?
I reluctantly joined twitter in the hope of connecting with people that would be interested in my hobby work. Unless something I was doing was tacking onto something bigger, nobody saw it.
Here people see it. Plus I see things like the cool music of @kevin-gallant.bsky.social
I reluctantly joined twitter in the hope of connecting with people that would be interested in my hobby work. Unless something I was doing was tacking onto something bigger, nobody saw it.
Here people see it. Plus I see things like the cool music of @kevin-gallant.bsky.social
May 3, 2025 at 10:29 PM
Why do I love bluesky?
I reluctantly joined twitter in the hope of connecting with people that would be interested in my hobby work. Unless something I was doing was tacking onto something bigger, nobody saw it.
Here people see it. Plus I see things like the cool music of @kevin-gallant.bsky.social
I reluctantly joined twitter in the hope of connecting with people that would be interested in my hobby work. Unless something I was doing was tacking onto something bigger, nobody saw it.
Here people see it. Plus I see things like the cool music of @kevin-gallant.bsky.social
Tone check please? Do you get what I'm trying to do? Do you get the sense that it will be verbose and annoying at times, but at least I'll try to have fun with it?
May 3, 2025 at 10:01 PM
Tone check please? Do you get what I'm trying to do? Do you get the sense that it will be verbose and annoying at times, but at least I'll try to have fun with it?
Does anybody have a good resource explaining math in terms of category theory from the ground up? A loop of:
Start with as little information as possible
what can we do with that information
when we run out of things to do, what are the smallest pieces of information we can add to do something new
Start with as little information as possible
what can we do with that information
when we run out of things to do, what are the smallest pieces of information we can add to do something new
May 3, 2025 at 4:04 PM
Does anybody have a good resource explaining math in terms of category theory from the ground up? A loop of:
Start with as little information as possible
what can we do with that information
when we run out of things to do, what are the smallest pieces of information we can add to do something new
Start with as little information as possible
what can we do with that information
when we run out of things to do, what are the smallest pieces of information we can add to do something new
Easter is his third favorite holiday.
April 21, 2025 at 12:37 AM
Easter is his third favorite holiday.
I'm curious, do many other people often write functions with a placeholder name and then use the implementation to figure out what to call it?
Anecdotally, most people can't figure out what or how to implement without a good name first. Am I weird or just not swimming in the right ponds?
Anecdotally, most people can't figure out what or how to implement without a good name first. Am I weird or just not swimming in the right ponds?
April 15, 2025 at 11:03 PM
I'm curious, do many other people often write functions with a placeholder name and then use the implementation to figure out what to call it?
Anecdotally, most people can't figure out what or how to implement without a good name first. Am I weird or just not swimming in the right ponds?
Anecdotally, most people can't figure out what or how to implement without a good name first. Am I weird or just not swimming in the right ponds?
I had to do the back road shuffle today because traffic was fubar. Totally worth it because I found an outdoor market with this friendly concierge. He seemed particularly eager to point out the okra, tomatillos, and pearl tomatoes, so I made a sour bindi masala
April 11, 2025 at 1:44 AM
I had to do the back road shuffle today because traffic was fubar. Totally worth it because I found an outdoor market with this friendly concierge. He seemed particularly eager to point out the okra, tomatillos, and pearl tomatoes, so I made a sour bindi masala
Stupid mocking bird imitating the alarm I snoozed.
March 17, 2025 at 11:24 AM
Stupid mocking bird imitating the alarm I snoozed.
March 16, 2025 at 4:22 PM
Every once in a while, I like to take a minute to appreciate languages with powerful type systems. I know it is nothing new, but I'm happy I can parameterize a type by an AST
![def dist : MeasureUnit "distance" "feet" Float := ⟨⟨8⟩⟩
def secs : MeasureUnit "time" "s" Float := ⟨⟨2⟩⟩
def rate := dist / secs
def rateExplicit : MeasureUnit ("distiance"/"time") ("feet"/"s") Nat := 5
#eval rate
#eval rateExplicit
#eval (5: MeasureUnit "distance" "feet" Nat) * (3: MeasureUnit "pressure" "pounds" Nat) * 10
#eval dist*dist
[{
"resource": "/home/hw/projects/lean/units/demo/Demo/Basic.lean",
"owner": "_generated_diagnostic_collection_name_#1",
"severity": 2,
"message": "4.000000 (feet per s)\n",
"source": "Lean 4",
"startLineNumber": 84,
"startColumn": 1,
"endLineNumber": 84,
"endColumn": 6
},{
"resource": "/home/hw/projects/lean/units/demo/Demo/Basic.lean",
"owner": "_generated_diagnostic_collection_name_#1",
"severity": 2,
"message": "5(feet per s)\n",
"source": "Lean 4",
"startLineNumber": 85,
"startColumn": 1,
"endLineNumber": 85,
"endColumn": 6
},{
"resource": "/home/hw/projects/lean/units/demo/Demo/Basic.lean",
"owner": "_generated_diagnostic_collection_name_#1",
"severity": 2,
"message": "150 (feet pounds)\n",
"source": "Lean 4",
"startLineNumber": 86,
"startColumn": 1,
"endLineNumber": 86,
"endColumn": 6
},{
"resource": "/home/hw/projects/lean/units/demo/Demo/Basic.lean",
"owner": "_generated_diagnostic_collection_name_#1",
"severity": 2,
"message": "64.000000 feet^2\n",
"source": "Lean 4",
"startLineNumber": 87,
"startColumn": 1,
"endLineNumber": 87,
"endColumn": 6
}]](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:qyv3dwfsr3ush5bt4vjgii2g/bafkreidsbadttyakr7ox2nclkwwfkhu2bbx25vjvgwzfc5m5qqzoyollnu@jpeg)
March 15, 2025 at 12:24 AM
Every once in a while, I like to take a minute to appreciate languages with powerful type systems. I know it is nothing new, but I'm happy I can parameterize a type by an AST
Brother and sister first time playing together. Doing an impromptu unrehearsed set to fill an empty slot at the gasparilla arts festival. I'm glad they picked a simple song to lead with
March 2, 2025 at 6:20 PM
Brother and sister first time playing together. Doing an impromptu unrehearsed set to fill an empty slot at the gasparilla arts festival. I'm glad they picked a simple song to lead with