{{ message }}

Instantly share code, notes, and snippets.

brendanzab/combining-pi-and-simga.md

Last active Apr 20, 2020
Probably a terrible idea

Combining Pi and Sigma types?

```-- id : forall a. a -> a
-- id x = x

id : type [
in A : Type,
in a : A,
out a' : A,
]
id = elem [
a' = a,
]

test-id-1 : Int
test-id-1 = id.(A = Int, a = 23).a'

test-id-2 : String
test-id-2 = id.(a = "hello").a'```
```-- some-fun : exists a. a -> a
-- some-fun True = False
-- some-fun False = True

some-fun : type [
out A : Type,
in a : A,
out a' : A,
]
some-fun = elem [
out A = Bool,
out a' = match a {
True => False,
False => True,
},
]```

How do we actually use this?

Records

```Point : Type
Point = type [
out x : Int,
out y : Int,
]

my-point : Point
my-point = elem [
x = 1,
y = 3,
]

test-x : Int
test-x = my-point.x

test-y : Int
test-y = my-point.y```

Parametrised records

```Point : Type
Point = type [
in A : Type,
out x : A,
out y : A,
]

my-point : Point.(A = Int)
my-point = elem [
out x = 1,
out y = 3,
]

test-x : Int
test-x = my-point.x

test-y : Int
test-y = my-point.y```

From Pikelet to this weird language

Pikelet Weird graph language
`Fun (A : Type) (a : A) -> A` `type [ in A : Type, in a : A, out a' : A ]`
`fun _ a => a` `elem [ a' = a ]`
`id String "hello"` `id.(A = String, a = "hello").a'`
`Record { A : Type, a : A }` `type [ out A : Type, out a : A ]`
`record { A = String, a = "hello" }` `elem [ A = String, a = "hello" ]`
`data.a` `data.a`
`let record { A, a } = data in ...` `data.(A = A, a = a, ...)`

Evaluation:

``````[ (l = term)... ].(l' = term')  -->  [ (l = term[l' / term'])... ]
[ (l = term)... ].l             -->  term
...
``````

Graph serialization

In the following, names starting with `\$` should be auto-generated ids. We use identifiers for readability, however.

The graph as a JSON tree:

```{
\$prelude : {
"pikelet.documentation.name": {
"pikelet.locale.en": "prelude"
},
"pikelet.documentation.short-description": {
"pikelet.locale.en": ["A collection of handy general purpose things."]
},
"pikelet.element": {
\$prelude.semigroup: {
"pikelet.documentation.name": {
"pikelet.locale.en": "semigroup"
},
"pikelet.element": {
\$prelude.semigroup.carrier: {
"pikelet.documentation.name": {
"pikelet.locale.en": "carrier"
},
"pikelet.type": \$pikelet.universe,
},
\$prelude.semigroup.append: {
"pikelet.documentation.name": {
"pikelet.locale.en": "append"
},
"pikelet.type": {
\$prelude.semigroup.input0: {
"pikelet.mode": \$pikelet.mode.input,
"pikelet.type": \$prelude.semigroup.carrier
},
\$prelude.semigroup.input1: {
"pikelet.mode": \$pikelet.mode.input,
"pikelet.type": \$prelude.semigroup.carrier
},
\$prelude.semigroup.output: {
"pikelet.mode": \$pikelet.mode.output,
"pikelet.type": \$prelude.semigroup.carrier
}
}
}
}
},
\$prelude.monoid: {
"pikelet.documentation.name": {
"pikelet.locale.en": "monoid"
},
"pikelet.element": {
\$prelude.monoid.semigroup: {
"pikelet.type": \$prelude.semigroup
},
\$prelude.monoid.empty: {
"pikelet.documentation.name": {
"pikelet.locale.en": "empty"
},
"pikelet.type": [
\$prelude.monoid.semigroup,
\$prelude.semigroup.carrier
]
}
}
},
\$prelude.id: {
"pikelet.documentation.name": {
"pikelet.locale.en": "identity"
},
"pikelet.documentation.short-description": {
"pikelet.locale.en": [
"A function where",
\$prelude.id.input,
"is always defined to be equal to",
\$prelude.id.output,
"."
]
},
"pikelet.type": {
\$prelude.id.type: {
"pikelet.mode": \$pikelet.mode.input,
"pikelet.type": \$pikelet.universe
},
\$prelude.id.input: {
"pikelet.mode": \$pikelet.mode.input,
"pikelet.type": \$prelude.id.type
},
\$prelude.id.output: {
"pikelet.mode": \$pikelet.mode.output,
"pikelet.type": \$prelude.id.type
}
},
"pikelet.element": {
?
}
}
}
}
}```

Perhaps one could build up the graph using a sequence of commands:

``````pikelet.id(\$pikelet.universe).
pikelet.id(\$prelude).
pikelet.id(\$prelude.semigroup).
pikelet.id(\$prelude.monoid).
pikelet.id(\$prelude.carrier).
pikelet.id(\$prelude.append).
pikelet.id(\$prelude.empty).
pikelet.id(\$prelude.id).
pikelet.id(\$prelude.always).

pikelet.documentation.name(\$type, { "en" = "type" }).
pikelet.documentation.name(\$prelude, { "en" = "prelude" }).
pikelet.documentation.name(\$prelude.semigroup, { "en" = "semigroup" }).
pikelet.documentation.name(\$prelude.monoid, { "en" = "monoid" }).
pikelet.documentation.name(\$prelude.carrier, { "en" = "carrier" }).
pikelet.documentation.name(\$prelude.append, { "en" = "append" }).
pikelet.documentation.name(\$prelude.empty, { "en" = "empty" }).
pikelet.documentation.name(\$prelude.id, { "en" = "identity" }).
pikelet.documentation.name(\$prelude.always, { "en" = "always" }).

pikelet.documentation.short-description(\$type, { "en" = "The type of types." }).
pikelet.documentation.short-description(\$prelude, { "en" = "A collection of handy general purpose things." }).
pikelet.documentation.short-description(\$prelude.semigroup, { "en" = "..." }).
pikelet.documentation.short-description(\$prelude.monoid, { "en" = "..." }).

pikelet.type(\$prelude, ?).
pikelet.type(\$prelude.semigroup, \$pikelet.universe).
pikelet.type(\$prelude.monoid, \$pikelet.universe).
pikelet.type(\$prelude.carrier, \$pikelet.universe).
pikelet.type(\$prelude.append, ?).
pikelet.type(\$prelude.empty, ?).

pikelet.element(\$prelude, \$prelude.semigroup).
pikelet.element(\$prelude, \$prelude.monoid).
pikelet.element(\$prelude.semigroup, \$prelude.carrier).
pikelet.element(\$prelude.semigroup, \$prelude.append).
pikelet.element(\$prelude.monoid, \$prelude.empty).
``````