typefuck-haskell - GitLite

KO | EN

gitlite — search

#javascript #python #ai #typescript #go #golang #android #windows #awesome #vue #pytorch #security #mcp #ios

typefuck-haskell

(★ 17)

Typelevel Brainfuck; Brainfuck implemented solely in Haskell's type system (no TemplateHaskell)

typefuck-haskell 최신버젼 다운로드

최종 버전 다운로드 (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# Typefuck (Haskell edition)

(inspired by [susisu's Typescript-edition typefuck](https://github.com/susisu/typefuck))

This Typefuck also runs solely in Haskell's type system, though (at least I think, as I haven't 
looked deeply into their code) it operates a bit differently than susisu's.

## (Roughly) How it works

The state of the program is managed by three main types:

```hs
{- | An efficient way to move forwards and backwards through some list
   (N.B. index == length preceeding) -}
type Cursor a = 
  ( Nat -- ^ The index of the currently selected thing
  , [a] -- ^ The preceeding things
  ,  a  -- ^ The thing the cursor is currently pointing at
  , [a] -- ^ The succeeding things
  )

{- | An association list to hold the index of each open bracket and its closing counterpart -}
type BracketLUT = [(Nat, Nat)]

{- | The state of the brainfuck engine -}
type TFState = 
  ( Cursor Char -- ^ The cursor for moving through the code
  , Cursor Nat  -- ^ The cursor for the memory tape
  , Symbol      -- ^ The input to the program
  , Symbol      -- ^ The output for the program
  , BracketLUT  -- ^ The aforementioned LUT for the []s
  )
```

and the rest is basically mutually-recursive type-family spam, which you can read
through as you please.

The tape is (hack-ily) generated through an external haskell script which creates
the file which contains the tape (more on that later).

I also had to manually implement versions of + and - that would overflow/underflow
to emulate ubyte-sized cells:

```hs
type family (a :: Nat) -~ (b :: Nat) :: Nat where
  a -~ b = UnderflowingSub' (CmpNat a b) a b

type family UnderflowingSub' (ord :: Ordering) (a :: Nat) (b :: Nat) where
  UnderflowingSub' 'LT a b = 256 - (b - a)
  UnderflowingSub'  _  a b = a - b

type family (a :: Nat) +~ (b :: Nat) :: Nat where
  a +~ b = Mod (a + b) 256
```

## Using it for yourself

To run this, you need to have at the very least `cabal` installed, but it'd be in your
favor to also have `make` + `bash` (or a compatable shell) up and running. `node` or 
(what I use) `bun` are also used for tests.

### Setting up the tape

The tape should already be pregenerated with 10 0s; however, you can generate
a tape with the command `make tape TAPE="<list_gen>"` where `<list_gen>` is some
expression that generates a haskell list. Examples include
  - `TAPE="[1, 2, 3]"`
  - `TAPE="replicate 10 0"`
  - `TAPE="[2 * x | x <- [1..10], mod x 2 == 0]"`

and it generates a file like so:

```hs
module TF.Generated.Tape where
type Tape = '[0,0,0,0,0,0,0,0,0,0]
```

If, for some reason, you can't use the command line utility, you can just manually generate
the list yourself (make sure you don't forget to use the `'`!)

Disclaimer: you're free to generate long tapes, but if you go too long, you'd risk being overtaken
by the heat-death of the universe lol

### Actually running Typefuck

My recommended way you use typefuck (if you're just type-fucking around) is to use `make repl` (`cabal repl app`),
`import TF.Core`, and `:k! RunTF "<code>" "<input>"`:

```hs
me@t:~/projects/typefuck-haskell$ make repl
<...>
λ> import TF.Core
λ> :k! RunTF ",." "a"
RunTF ",." "a" :: ghc-prim:GHC.Types.Symbol
= "a"
λ> :k! RunTF "++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-.<.+++.------.--------.>>+." ""
<...>
= "Hello World!"
λ>
```

You can also use `reifySF` from `Utils` to create a concrete string, but that takes
*much* longer to generate any non-trivial programs

```hs
λ> symbolVal $ Proxy @(RunTF ",." "a")
"a"
λ> reifyTF @",." @"a"
"a"
```

### "Open" vs "Closed" inputs

In the event that your input-requiring code isn't working when it should be (e.g. printing empty input), there's a
chance it's because you're using loops but your input isn't `NUL`-terminated (i.e. it doesn't read in a closing `'\0'`
input to stop the loop). In that case, try changing `"Hello!"` to `"Hello!\0"`.

By default, when TF runs out of input, it just prints what input it has already (to emulate an interactive interpreter
just pausing, waiting for input).

### Running the tests

You can run the tests with `make test` w/ bun/node (or manually executing `spec/run-tests.mjs`).
You can add your own tests to `spec/tests.json` as you please.

## Disclaimer

I basically wrote this in a night or two so there may be some minor bugs and things that could be more efficient,
but I'm looking to fix them as I get time and motivation. Feel free to contribute!