I chatted with Sean today for a while and he left me with a cute types puzzle. The puzzle is, assign types to the ?s in the signature
```sig
val blank : ?
val binop : (int * int -> int) -> ?
val unop : (int -> int) -> ?
val const : int -> ?
val eval : ?
end
```

and implement it in a structure S such that the following makes sense:
```open S
(* expression with holes: [ ] + (~[ ] + (2 * [ ])) *)
val f = eval (binop (op+) blank (binop (op+) (unop (op~) blank) (binop (op *) blank (const 2))))
val _ = print (Int.toString (f 100 2 3000)) (* prints 100 + (~2 + (2 * 3000)) = 6098 *)
val _ = print "\n"
```

What's going on here is f builds up an expression tree out of binary and unary operators and integer constants and blank holes, calls eval on it, and this has the type
int -> int -> int -> int
which is a curried type with three integer arguments, equal to the number of occurrences of "blank" in the definition of f.

But how can you get eval to have a type that always has one curried argument for each blank, and in fact evaluates the right expression?

The essential trick is taken from some Janest code sean showed me as a hint:
https://bitbucket.org/yminsky/ocaml-core/src/8808e3a2571f/base/core/extended/lib/core_command.mli
I think it's a really cute cps-y thing to do. I think I remember this sort of thing being done to make a type-safe printf.
```structure S :>
sig
type ('a, 'b) t
val blank : (int -> 'a, 'a) t
val binop : (int * int -> int) -> ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
val unop : (int -> int) -> ('a, 'b) t -> ('a, 'b) t
val const : int -> ('a, 'a) t
val eval : ('a, int) t -> 'a
end
=
struct
type ('a, 'b) t = (int -> 'b) -> 'a
fun blank x = x
fun binop f t1 t2 k = t1 (fn x => t2 (fn y => k (f (x, y))))
fun unop f t k = t (fn x => k (f x))
fun const n k = k n
fun eval f = f (fn x => x)
end

structure T =
struct

open S
val f = eval (binop (op+) blank (binop (op+) (unop (op~) blank) (binop (op * ) blank (const 2))))
val _ = print (Int.toString (f 100 2 3000))
val _ = print "\n"
end
```

Tags:
• (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

Error

Anonymous comments are disabled in this journal

default userpic

Your reply will be screened

Your IP address will be recorded

• 13 comments
• (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…