rybla

module Languages.IntrinsicallyTypedLambdaCalculus where

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

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

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

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 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

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

(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

--------------------------------------------------------------------------------
-- 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

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

{-# LANGUAGE GADTs, KindSignatures, DataKinds, RankNTypes, TypeFamilies, TypeFamilyDependencies, AllowAmbiguousTypes, ScopedTypeVariables #-}

module OverloadSingletonI where

import Prelude hiding (negate)

data OverloadMode = NegateInt | NegateBool 

data SOverloadMode :: OverloadMode -> * -> * where
  SNegateInt :: SOverloadMode NegateInt (Int -> Int)

rybla

module Inductive where

open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Product
open import Data.Sum

module Inductive

rybla

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module InaccessiblePattern where