Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Updates on the Pikelet Programming Language
marp theme
true
uncover

Pikelet status update

Brendan Zabarauskas

31/08/2020

Pikelet Mascot


What is Pikelet


What is Pikelet

  • helps temper my desire to turn my work project into a general purpose language
  • also helps me scratch a few itches
  • kind of slow going, chipping away at it over time

What is Pikelet

  • annoyances with Rust
    • inconsistencies between the type language and the term language
    • difficult to make nice libraries based on mathematical patterns
    • kind of ugly
  • interest in 1ML
  • desire to see dependent types be:
    • useful for practical programming
    • be useful for low level systems programming
    • friendly to use and accessible (easy to install, good error messages, good tooling, etc.)

record {
    Category : Type^1 = Record {
        Object : Type,
        Arrow : Object -> Object -> Type,
        id : Fun (A : Object) -> Arrow A A,
        seq : Fun (A B C : Object) ->
          Arrow A B -> Arrow B C -> Arrow A C,
    },

    Functor : Type^1 = Record {
        Source : Category,
        Target : Category,
        Map : Source.Object -> Target.Object,
        map : Fun (A B : Source.Object) ->
          Source.Arrow A B -> Target.Arrow (Map A) (Map B),
    },
}

Non-Goals (for now)

  • proofs and formal verification (in Pikelet)
  • rigorous metatheory (about Pikelet)
  • above could be done later, but not my focus right now

Pikelet/next


Pikelet/next

  • dependent function types
  • dependent record types
  • universe levels with a lifting operator
  • constants for integer, floating point, characters, strings, etc.

Pikelet/next

  • New, nicely organised modules
    pikelet
    ├── lang
    │   ├── surface
    │   ├── core
    │   │   ├── semantics
    │   │   └── typing
    │   ├── anf [TODO]
    │   └── cc [TODO]
    └── pass
        ├── surface_to_core
        │   ├── pattern_compiler [TODO]
        │   └── unification [TODO]
        ├── core_to_surface
        ├── core_to_anf [TODO: A-normal form translation]
        └── anf_to_cc [TODO: closure conversion]
    

Pikelet/next


What's next?

  • enumeration sets:
    record {
        Option : Type -> Type,
        Option A = Record {
            tag : Enum { some, none },
            data : match tag {
                some => A,
                none => Record {},
            },
        },
    }
    

What's next?

  • elaboration of implicit arguments (see Andras Korvacs work)
    record {
        id : Fun {A : Type} -> A -> A,
        id {A} a = a,
    
        test : S32,
        test = id 1,   -- elaborates to `id {A = S32} 1`
    }
    

What's next?

  • let expressions
    let
        x : S32 = 1
        y : S32 = 3 * x
    in
        x * y
    
  • elaborates to:
    (record { x = 1, y = 3 * x, default = x * y } :
      Record { x : S32, y : S32, default : S32 })
        .default
    
  • this is kind of like what 1ML does

What's next?


Research that I'm keeping an eye on


Weird ideas


Weird ideas

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment