search

strangemonad / runway

Domain models and their values
1 stars 0 forks source link

readme

Runway

Domain models and their values

TODO

Syntax design

Language / type system Ideas

Open questions:

Implementation ideas

Encode target language features as types / functors https://brianmckenna.org/blog/polymorphic_programming

Language

A language for expressing and communicating ideas but not how to define the processes behind them.

Primitives / builtin

Note: separation of primitive types vs primitive vals

Syntax "pronounciation" guide

Here's a few snippets of runway code and how to informally read it (in our heads or aloud). We often want to know how to "pronounce" phrases without getting bogged down in the technicalities of the actual math and type theory.

We'll leave pointers about the underlying terminology so the curious know where to look.

Stating things we know

The main idea is that we want to simply stating things we know (or might want to know). We get the computer fill in any gaps or point out inconsistencies.

Asside: Statements about things we know are called judgments.

We have 2 very basic kinds of statements that express 2 primitive relationships

When you see = think "is". Left to right: "is equal to", "is defined to be", "is identical to", "is the same as", "is identified with", "is solved by" Right to left: "is the definition of", "is the solution to", "can stand for", "can be substituted for"

n = 5

name = "James"

It's tempting to think we're just assigning values to constants but its more useful to think of identification as a solution to an equation like you might remember from high-shool math (e.g. x = 4y + 5). You're stating a relationship about the left and right hand sides of the equation. In the simple cases above the solution is trivial assignment.

When you see : think "is a" Left to right: "is a member of", "is an element of" Rgith to left: xxx

n : Int

Random syntax thoughts

Foo = (Int, Int)

Foo : Type

On the fly tags (assuming Foo enumerated data type)? How does twelf's nat work under the hood?

want something like:

Nat : Type z : Nat s : Nat -> Nat %freeze (the structural inductive type definition but not other uses of nat)

Nat : Type = { z : Nat s : Nat -> Nat }

What about Nat = {z, s: Nat -> Nat} Nat : Type = {z, s: Nat -> Nat} Nat = {z: Nat, s: Nat -> Nat} Nat = {z, s(n:Nat)} Nat = {z, s } Nat = {z, s : Nat } Nat = {z : Nat , s : Nat } Nat : Type = { z : Nat s : Nat }

eg: Bool = {True, False} Bool = {True. False.}

Foo_Tag : Type c1:Foo_Tag c2:Foo_Tag %freeze

// Most direct Foo_Tag : Type = { c1:Foo_Tag c2:Foo_Tag }

// ? Foo_Tag = { c1:Foo_Tag c2:Foo_Tag } : Type // ?

Foo_Tag : Type = {c1, c2} Foo_Tag = {c1, c2} : Type Foo_Tag:Type = c1 | c2

// type alias is not what we want Person = (name:String, age:Int)

Person = { name: String age: Int }

// ^^^ incompatible with vvv // ie: the Foo : Type = sig form Foo = { Foob: (i:Int) -> Foo Fab: (s:String, i:Int) -> Foo }

Non-disjoint sum is common - should it be streamlined?

Person = { new : (name:String, age:Int) -> Person }

p = Person.new(....) // vs p = Person(...)

Tedious to always 1) choose a name for the constructor 2) Specify the return type 3) the call site name isn't what we want for the definition site // alternatives new, of, from, with, as, init, get

do we want an alternate form?

Person = data { | _ of (name:String, age:Int) }

Bool = { true: bool false: bool }

Bool = data { | true | false }

or also allow a one liner Bool = data {true | false} or just Bool = data true | false

MaybeInt = { none: MaybeInt some: Int -> MaybeInt }

MaybeInt = data { | none | some(Int) }

// Does the above allow proper induction? // The above feels too nuts and bolts, I don't really care about a tuple of value constructors // It also looses the idea of a tagged tuple

Foo = { | Foob (i:Int) | Floop (i:Int) | Fab (s:String, i:Int) }

// Does the following allow any form of data abstraction? Foo = Foob (i:Int) | Fab (s:String, i:Int)

Foo = data | Foob (i:Int) | Fab (s:String, i:Int)

Foo = | Foob (i:Int) | Fab (s:String, i:Int)

Elaborates to => Option 1) Person: Type Person.new: (name:String, age:Int) -> Person

Option 2)

Questions about data types

"Hypothetical" type judgements

Best shown by example:

```
List <elem:Type> : Type
> List : (elem:Type) -> Type

List(String)
> List(String) : Type

StringList = List(String)
> StringList : ??? List(String)

l : StringList
> l : List(String)
```

Pattern:

Foo <t:Type> : Type

Read typically:

Read logically:

Elaborates to: => Foo : (t:Type) -> Type => Foo(String) : Type

Note: Foo is a type constructor (in the sense that it's a function Type -> Type) Just move the : for the curried vs un-curried form.

Note: Functions capture the concept of hypothetical

More examples List <elem:Type> : Type => List : (elem:Type) -> Type Vec <elem:Type, count:Int> : Type => `e

Reads Foo

// Tuple is a kind family Tuple0: () -> Type Tuple1: Type -> Type Tuple2: Type -> Type -> Type

// Foo:Tuple<Type, Type>

tuple: [Type -> Type

type Foo = (int, int) Foo = (int, int)

Foo : (Type, Type) = (Int, Int) // do we also also have a TyCon Foo:Int -> Int -> Type

(1,2):Foo (1,2):(int, int)

bar = 5

bar = 5 : Int

// ie: bar : Int and 5 : // ie = where = <t:Type> : (t, t) -> Bool

Person = (name: String)

Person : Type = (name : String) did I introduce a tyocon in the equation above? Person(name = foo)?

Maybe: -> Type type Maybe

Maybe = data { | None | Some Elem }

Mabye : Type -> Type None : Maybe Some