rybla

open import Data.Nat

data Vec : ℕ → Set → Set where
  nil : ∀ {A} → Vec 0 A
  cons : ∀ {A n} → A → Vec n A → Vec (suc n) A

record Traversable (F : Set → Set) : Set1 where
  field
    traverse : ∀ {S T : Set} {G : Set → Set} → (S → G T) → F S → G (F T)

rybla

--------------------------------------------------------------------------------
-- Tree
--------------------------------------------------------------------------------
data Tree a
  = Tree a (Array (Tree a))

instance functorTree :: Functor Tree where
  map f (Tree a ts) = Tree (f a) (map f <$> ts)

instance applyTree :: Apply Tree where

rybla

(based on a conversation I had with Jacob Prinz)

SYSTEM

You are a knowledgeable programming languages assistant. You help the user analyze a new programming language.

USER

Slrj is a new programming language. The grammar of Slrj expressions is defined as follows, where "x" is any Slrj expression, and "A", "B", and "C" are atomic values.

rybla

Based on Slrj.chat.md; inspired by a conversation with aljce

User

You are a knowledgeable programming languages assistant. You help the user analyze a new programming language.

Aljc is a new programming language. The grammar of Aljc expressions is defined as follows, where x is any Aljc expression and A, B, and C are atomic values.

x ::= A | B | C | (x x)

rybla

module Data.MyExistsConstrained where

import Prelude
import Unsafe.Coerce (unsafeCoerce)

-- Suppose you want to use an existentially-quantified type. You can use the
-- `exists` package, which defines `Exists` likes so:

foreign import data Exists :: (Type -> Type) -> Type

rybla

/*
The idea of this implementation is that a row (`Row`) serves as the
specification of either:
- a record (`Record<T extends Row>`) which is an object that, for each of the
  elements of the row, has a key-value mapping from the element's tag to the
  element's domain
- a variant (`Variant<T extends Row>`) which is a union of the row elements.
*/

type Tuple = any[]

rybla

module Languages.IntrinsicallyTypedLambdaCalculus where

import Prelude hiding (($), type (~>))

import Data.Symbol (class IsSymbol)
import Prim.Row (class Cons)
import Type.Proxy (Proxy(..))

-- =============================================================================

rybla

// while iterating, have a `mut bindings: Vec<Bindings>`
// have a structure of Scopes that contain references to values in `bindings`
// a Binding doesn't refer to a Scope
// at the end, return `bindings`, so Scopes cannot own anything in bindings

// mutable reference is a subtype of immutable reference
fn example<'source>(
    bindings: &mut Vec<Box<Binding<'source>>>,
    names: Vec<&'source str>,
) {

rybla

module Main where

import Prelude

import Effect (Effect)
import Effect.Aff.Class (class MonadAff)
import Halogen as H
import Halogen.Aff as HA
import Halogen.HTML as HH
import Halogen.VDom.Driver as HVD

rybla

import Prelude

import Effect (Effect)
import Effect.Aff (launchAff_)
import Effect.Class (liftEffect)
import Effect.Class.Console as Console
import Node.Encoding (Encoding(..))
import Node.EventEmitter (on_, once_)
import Node.FS.Sync as FS
import Node.HTTP (createServer)