Probably a terrible idea

combining-pi-and-simga.md

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

See also

• An old sketch: https://twitter.com/brendanzab/status/1191931829785432066
• Another idea: https://gist.github.com/brendanzab/63c2d42c41c95922c0ee98e6e7a10cbb

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