Fork me on GitHub
#core-typed
<
2020-02-16
>
ambrosebs00:02:17

fwiw I ported something like #lang functionality to clojure. kind of lost interest because I didn't feel there was much demand for it https://github.com/typedclojure/core.typed.lang.jvm

ambrosebs00:02:52

but I'm personally interested in preserving clojure's evaluation model as-is as much as possible, it certainly has it's advantages. very simple.

ambrosebs00:02:14

it breaks down when you need to write macro-generating macros. but that's the only limit I've come across in practice

ambrosebs00:02:27

and macros aren't that important in clojure anyway

whilo01:02:52

yes, that is very different in racket.

whilo01:02:04

do you have a sense of the parts of racket you would like to see ported over?

whilo01:02:26

people here use redex a lot to prototype languages as it seems, i have not used it it yet

ambrosebs01:02:16

I'm a big fan of clojure. I'm not glamouring for anything in particular from racket. I want the best parts of Typed Racket and turnstile, but tailored precisely to clojure

ambrosebs01:02:05

anything that helps me understand clojure more deeply, I'm really into

ambrosebs01:02:03

and basically everything I've learnt has been from contrasting it with racket/typed racket. so I find racket useful and interesting from that perspective

whilo01:02:03

makes sense

whilo01:02:28

sorry, not the right link

whilo01:02:51

i mean "Dependent Type Systems as Macros" on this page, somehow it is not part of the URL

ambrosebs01:02:02

oh yea they finally got it published

ambrosebs01:02:04

really exciting

whilo01:02:10

this is an extension of turnstyle called turnstyle+

ambrosebs01:02:51

haven't read it yet

whilo01:02:55

yes, i am meeting william several times a week in reading groups, we are going through his thesis at the moment

ambrosebs01:02:27

my wife worked on cur for a few months about a year ago

ambrosebs01:02:52

so I got to hear about some progress and their frustrations in publishing a previous version of that paper

ambrosebs01:02:08

basically reviewers saying "why isn't this agda"

ambrosebs01:02:18

and "this is only possible in racket => boring"

ambrosebs01:02:39

that's cool, is he presenting his own thesis?

whilo01:02:44

hehe, the PL community is more partisan than the ML community even

whilo01:02:58

we are sitting together and he is answering questions

whilo02:02:05

we go through it chapter by chapter

ambrosebs02:02:44

"Since dependently typed languages may evaluate expressions while type checking, checking dependent types with macros requires new macrology design patterns and abstractions for interleaving expansion, type checking, and evaluation"

ambrosebs02:02:00

sounds familiar..

ambrosebs02:02:52

probably should read this paper

ambrosebs02:02:44

tho I like to see what I invent before seeing prior research

ambrosebs02:02:03

I get tunnel vision once i see a solution

ambrosebs02:02:12

I'm also juggling expansion, type checing, evaluation, and symbolic excution

ambrosebs02:02:39

but it's basically the same thing I imagine. Just some extra details of clojure thrown in

ambrosebs02:02:21

turnstile+'s "evaluation" is probably just dependent type checking, and for me it's literally calling eval on a clojure form

ambrosebs02:02:46

so my symbolic execution is turntile+'s evaluation (probably)

whilo02:02:41

that makes sense. what would be necessary to make that extensible? i.e. being able to strengthen clojure semantics by adding annotations or additional derivations and being able to plug into your pipeline?

whilo02:02:07

i am building bayesian inference schemes that propagate measures through your code. there can be facts you know about these numeric entities or that you can add to description of algorithms, e.g. about convergence or resource usage, that could be automatically available to the type system.

whilo02:02:54

in a more commercial setting i imagine having world knowledge about the system and clients that are referred to in the types that might be provided through a database

whilo02:02:35

that is what we have been discussing with our cloud service provider client. in that setting you want to ensure static guarantees over your distributed system and would like to type check your infrastructure

whilo02:02:00

if the type information would be in something like a datalog database then this would be way easier

whilo02:02:41

if you can then write down rules with queries on the environment instead of using the clumsy PL notation, you could build much more refined type judgements as extensions and maybe make dependent types more accessible

whilo02:02:24

i can try to come up with more concrete examples, if this is still too vague

whilo02:02:25

i think most type system people work with functional languages, but are amazingly primitive when they deal with the description of the logic on the type system level. they mostly use adhoc encodings to describe the rules

ambrosebs02:02:36

I love concrete examples

whilo02:02:19

let's say you assign a memory limit to a client inside of your cloud system that you track in your client-related database. you also track the memory limits of all the docker containers you can spawn on the system with kybernetes. now you do runtime checks regularly to ensure that clients to do not violate their limit. nonetheless you write nontrivial code that does scheduling and cluster allocations and it would be nice if you could prove that it does not violate the memory limits provided to it in form of the database over clients and the database over cloud containers

whilo02:02:05

with client here i mean business client

whilo02:02:47

it is similar to the dependently typed example of checking shapes of arrays that are passed in at compile time and ensuring you do not access them out of bounds

whilo02:02:31

i am not sure whether this was super clear

ambrosebs02:02:55

I'm with you I think, how does that tie in with your extensibility q?

ambrosebs02:02:26

what are you extending?

whilo02:02:49

you can first collect and extract as much information as might be helpful in the database for the type environment and others and then right rules that make use of all this information

whilo02:02:18

type inference and execution is kind of interleaved in dependent types

whilo02:02:15

that means if you can extend your knowledge during execution by collecting information of the environment, proving certain things in a local scope becomes much easier

whilo02:02:53

maybe i am oversimplifying

whilo02:02:02

but i imagine having a kind of type checking be partially done at runtime, somewhat like gradual typing

whilo02:02:38

where runtime checks are introduced, but they could also then run a refined type inference to make sure that everything is adding up

ambrosebs02:02:39

I have no idea how to plug dependent type checking into runtime clojure evaluation

whilo02:02:11

do you have a typed eval?

ambrosebs02:02:16

and I guess that's the big distinction between my work and turnstile+? their evaluation is literally runtime?

ambrosebs02:02:35

probably not, what would that look like?

ambrosebs02:02:43

like, eval with an expected type?

ambrosebs02:02:04

my "evaluation" is symbolic

ambrosebs02:02:30

are you asking if typed clojure implements an interpreter?

whilo02:02:37

i am not sure whether their evaluation is at runtime

ambrosebs02:02:53

hmm ok. I thought that's what dependent type checking meant

whilo02:02:58

i am asking whether you could rewrite part of the code before it goes into eval

ambrosebs02:02:01

not well versed in it myself

whilo02:02:45

i think so too, but i have to check more precisely what they do. we are not at turnstyle yet in the reading group, i have just heard about the paper a few weeks ago

ambrosebs02:02:29

yea you can emit custom code from a typing rule. but that's not a good idea because (unlike turnstile) core.typed isn't always in charge of expansion

ambrosebs02:02:53

which is why I dabbled in #lang's for clojure, to hook core.typed into load/require

ambrosebs02:02:34

well, if you used a typed #lang in clojure that always enforced type checking on load, it would be a good idea

ambrosebs02:02:57

and the extension points would be similar to turnstile's I imagine

whilo02:02:51

to rephrase on a high-level, i think an extensible static analysis stack allows to join the type inference with a general proof system over a rich set of domains if the basis for the logical inference rules is a shared logic programming language like datalog

whilo02:02:32

datalog is also used for reachability analysis and there are some attempts to use it for type systems, but in clojure land we also have our domain data in a powerful datalog database

whilo02:02:57

(i.e. datomic)

whilo02:02:39

what do you mean with extension points exactly?

whilo02:02:42

watching their talk now

ambrosebs02:02:04

like you can define a typing rule for macro invocations and primitives

ambrosebs02:02:18

that's where you plug into the type checker

ambrosebs02:02:15

I'm not clear what exactly you want to "plug into my pipeline". the compilation of rules to datalog?

whilo02:02:04

i think the rules themselves could contain datalog, it would actually make more complicated rules more explicit

whilo02:02:29

at least i have found some of the notation changing between papers and confusing when the rules do tricky things

whilo02:02:44

i mean the environment is effectively a database

ambrosebs02:02:15

type environment?

ambrosebs02:02:42

sounds like occurrence typing where the environment is a set of propositions

ambrosebs02:02:58

at least it sits close to that in my brain

whilo02:02:22

can you describe this position a bit more?

ambrosebs02:02:01

yea so instead of the normal type environment which is a sequence of mappings from var=>type [x : Int, y : Bool], you use propositional logic to represent the current environment. atomic propositions are statements of the form "x is of type t". and you can && and || them any way you like

ambrosebs02:02:20

like {"x is type Int", "y is type Bool"} is a proposition env

ambrosebs02:02:30

and you would query the env to find the type of x

ambrosebs02:02:44

{"x is type Int", "y is type Bool"} |- x : Int

ambrosebs02:02:21

and the rule for looking up in the type environment does constraint solving (model checking IIRC?) to determine the type of x

ambrosebs02:02:43

you can have interesting props like ("x is type Int" || "y is type Bool")

ambrosebs02:02:57

and then if you type check (if (integer? x) e1 e2) you can update the then branch with the prop "x is type Int", which reduces the env to "x is type Int", and the else branch with !"x is type Int" (negation) which reduces env to "y is type Bool"

ambrosebs02:02:30

check out "Logical Types for Untypable Languages" Tobin-Hochstadt & Felleisen for intro

ambrosebs02:02:57

also Andrew M Kent has a bunch of ideas simplifying the original paper

ambrosebs02:02:19

so this sounds like adding statements to a database

ambrosebs02:02:39

and then querying the database to get the type of bindings at a particular context

ambrosebs02:02:54

the intro/elim rules sounds similar

ambrosebs02:02:58

for environments

whilo03:02:48

yes, that is very related, although Datalog itself provides a programming language to describe simple inference rules over relations extending on pure propositional logic. it is still first order though and some restrictions on mixing recursion with negation to stay terminating.

whilo03:02:43

it would be like a base language for inference that can be extended by more rules, either in datalog or by ones doing more fancy logical constraint resolution

ambrosebs03:02:05

that would be useful for implementing occurrence typing. I tried using minikanren to do it once https://github.com/frenchy64/miniKanren-occurrence-type-inferencer

ambrosebs03:02:58

erm that link might be garbage, can't find the original

whilo03:02:01

right. minikanren would be like prolog. the problem is that it does not necessarily terminate, so you could easily have an undecidable type system then

ambrosebs03:02:51

yea I had a hell of a time getting simple things to run quickly or even terminate

whilo03:02:21

yes, that looks very much like the same line of thought

whilo03:02:51

the very pragmatic benefit i see from using a datalog database, is that we know how to populate it from everywhere with information

whilo03:02:21

what is your opinion about this direction of thinking?

ambrosebs03:02:12

don't know datalog. I like the direction of somehwere inbetween hand-written and minikanren

whilo03:02:15

(or more precisely, datalog is compositional over multiple data sources, datahike for instance can join data from everywhere, locally, a cluster db or one running for another party on AWS)

whilo03:02:01

i think you still need to be able to write custom inference logic, because type systems very much are at the boundary of making logic programming tractably enough to handle programs

ambrosebs03:02:28

yea. it sounds challenging. I g2g tho, chat later!

whilo03:02:44

have a nice evening

whilo20:02:31

regarding that it would be challenging, i am mostly thinking of instead of storing the environment in a hash-map to store it in an in-memory datalog database (could be datascript) and just start with using the pull syntax to get items out, practically the same as for a hash-map. but once the environment is stored in that way, one would have the freedom to a) use datalog queries and rules selectively when a more complicated invariant is supposed to hold in the type environment and, independently, b) expose immutable snapshots of this environment also to the runtime code in case it declares its interest (intertwining compile and runtime more effectively).

whilo20:02:10

datascripts motto is literally to make using datalog as easy as using a hash-map 🙂

whilo20:02:21

(and as performant)

whilo20:02:11

the goal is by no means to write the full type system in datalog. it is not expressive enough for that