Iso a b is the type of an isomorphism between a and b.
:t MkIso
((a:Type) ?-> (b:Type) ?-> {bwd: b -> a & fwd: a -> b} -> Iso a b)
This is a normal ADT, and you can construct your own isomorphisms.
def cycle_three {a b c} : Iso (a & b & c) (b & c & a) =
MkIso {
fwd = \(a, b, c). (b, c, a)
, bwd = \(b, c, a). (a, b, c)
}
Isomorphisms can be applied with app_iso, applied in reverse with rev_iso,
and flipped with flip_iso
:p app_iso cycle_three (1, 2.0, 3)
(2., (3, 1))
:p rev_iso cycle_three (1, 2.0, 3)
(3, (1, 2.))
:p app_iso (flip_iso cycle_three) (1, 2.0, 3)
(3, (1, 2.))
They can also be composed with &>>:
:p app_iso (cycle_three &>> cycle_three) (1, 2.0, 3)
(3, (1, 2.))
:p app_iso (cycle_three &>> cycle_three &>> cycle_three) (1, 2.0, 3)
(1, (2., 3))
Note that we assume but do not check that the isomorphism is lawful (i.e.
app_iso iso $ rev_iso iso x == x for all x, or equivalently
iso &>> (flip_iso iso) == id_iso).
In addition, Dex will automatically write some useful isomorphisms for you
to extract fields from records and variants. There are four syntactic forms
that produce isos. We will start with the first two:
#x produces a "lens-like" record accessor Iso {x:a & ...r} (a & {&...r})#?x produces a "prism-like" variant matcher Iso {x:a | ...r} (a | {|...r})
%passes parse
:t #b :: Iso {a:Int & b:Float & c:Unit} _
(Iso {a: Int32 & b: Float32 & c: Unit} (Float32 & {a: Int32 & c: Unit}))
(MkIso {fwd=(\{b=x, ...r}. (,) x r), bwd=(\(x, r). {b=x, ...r})}
: Iso {a: Int & b: Float & c: Unit} _)
%passes parse
:t #?b :: Iso {a:Int | b:Float | c:Unit} _
(Iso {a: Int32 | b: Float32 | c: Unit} (Float32 | {a: Int32 | c: Unit}))
(MkIso
{fwd=(\v. case v
{| b = x |} -> (Left x)
{|b| ...r |} -> (Right r))
, bwd=(\v. case v
((Left x)) -> {| b = x |}
((Right r)) -> {|b| ...r |})}
: Iso {a: Int | b: Float | c: Unit} _)
There are also two "zipper" forms, described later on this page:
Record accessors and lens-like helpers
Record accessor isomorphisms can be passed into the helper function get_at:
:t get_at
((a:Type) ?-> (b:Type) ?-> (c:Type) ?-> (Iso a (b & c)) -> a -> b)
:p get_at #foo {foo=1, bar=2.0}
1
We can also do other types of things:
:p pop_at #foo {foo=1, bar=2.0}
{bar = 2.}
:p push_at #foo 3.0 {foo=1, bar=2.0}
{bar = 2., foo = 3., foo = 1}
:p set_at #foo 2 {foo=1, bar=2.0}
{bar = 2., foo = 2}
These helper functions work with any "lens-like" isomorphism. For instance,
we can select everything except for a particular field:
:t except_lens
((a:Type) ?-> (b:Type) ?-> (c:Type) ?-> (Iso a (b & c)) -> Iso a (c & b))
:p get_at (except_lens #foo) {foo=1, bar=2.0, baz=3}
{bar = 2., baz = 3}
Variant accessors and prism-like helpers
Similarly, there are prism-like helpers
:t match_with
((a:Type) ?-> (b:Type) ?-> (c:Type) ?-> (Iso a (b | c)) -> a -> Maybe b)
:t build_with
((a:Type) ?-> (b:Type) ?-> (c:Type) ?-> (Iso a (b | c)) -> b -> a)
which can be used with variant accessors or any other prism-like isomorphism:
:p match_with #?foo $ {|foo = 1|}::{foo:Int | bar:Float}
(Just 1)
:p match_with #?foo $ {|bar = 1.0|}::{foo:Int | bar:Float}
Nothing
:p build_with #?foo 3 :: {foo:Int | bar:Float}
{| foo = 3 |}
:p match_with (except_prism #?foo) $ {|bar = 1.0|}::{foo:Int | bar:Float}
(Just {| bar = 1. |})
Record zipper isomorphisms
The isomorphisms shown above are specialized for removing a single field from
an object. As such, they don't compose well when trying to work with more than
one field at a time. When using multiple fields, a better choice is to use
a "zipper isomorphism", which moves a subset of fields from one place to
another. For instance:
%passes parse
:t #&a :: Iso ({&} & {a:Int & b:Float & c:Unit}) _
(Iso
({&} & {a: Int32 & b: Float32 & c: Unit})
({a: Int32} & {b: Float32 & c: Unit}))
(MkIso
{fwd=(\({...l}, {a=x, ...r}). (,) {a=x, ...l} {...r})
, bwd=(\({a=x, ...l}, {...r}). (,) {...l} {a=x, ...r})}
: Iso ((&) {} {a: Int & b: Float & c: Unit}) _)
:t (#&a &>> #&b) :: Iso ({&} & {a:Int & b:Float & c:Unit}) _
(Iso
({&} & {a: Int32 & b: Float32 & c: Unit})
({a: Int32 & b: Float32} & {c: Unit}))
#&a and #&b are isomorphisms that move a given field from the record on the
right to the record on the left; when composed, they move both fields.
The main use for record zipper isomorphisms is to specify multiple named axes
when using a record type as an index set:
:t over_fields
((a:Type)
?-> (b:Type)
?-> (c:Type)
?-> (v:Type)
?-> (v#0:(Ix b))
?=> (v#1:(Ix c))
?=> (Iso ({&} & a) (b & c)) -> (_autoq:(Ix a)) ?=> (a => v) -> b => c => v)
Note that over_fields is just a simple wrapper combining split_r and
over_lens:
:t split_r
((a:Type) ?-> Iso a ({&} & a))
:t over_lens
((a:Type)
?-> (b:Type)
?-> (c:Type)
?-> (v:Type)
?-> (v#0:(Ix b))
?=> (v#1:(Ix c))
?=> (Iso a (b & c)) -> (_autoq:(Ix a)) ?=> (a => v) -> b => c => v)
over_lens alone can be used with any lens-like isomorphism, for instance an
ordinary record accessor lens.
def abc_to_tuple {a b c} : Iso {a:a & b:b & c:c} (c&b&a) =
fwd = \({a, b, c}). (c, b, a)
bwd = \(c, b, a). {a, b, c}
MkIso {fwd, bwd}
instance Ix {a:n & b:m & c:q} given {n m q} [Ix n, Ix m, Ix q]
size = size n * size m * size q
ordinal = ordinal <<< app_iso abc_to_tuple
unsafe_from_ordinal = unsafe_from_ordinal _ >>> rev_iso abc_to_tuple
def bc_to_pair {b c} : Iso {b:b & c:c} (c&b) =
fwd = \({b, c}). (c, b)
bwd = \(c, b). {b, c}
MkIso {fwd, bwd}
instance Ix {b:n & c:m} given {n m} [Ix n, Ix m]
size = size n * size m
ordinal = ordinal <<< app_iso bc_to_pair
unsafe_from_ordinal = unsafe_from_ordinal _ >>> rev_iso bc_to_pair
:p
x = for {a, b, c}:{a:Fin 2 & b:Fin 2 & c:Fin 2}.
ordinal a * 100 + ordinal b * 10 + ordinal c
over_lens #a x
[[0, 10, 1, 11], [100, 110, 101, 111]]
split_r can be used if you want to process multiple fields at once:
:p push_at (split_r &>> #&a &>> #&b) {a=1, b=2.0} {c=3, d=4.0}
{a = 1, b = 2., c = 3, d = 4.}
Variant zipper isomorphisms
Just as there are record zipper isomorphisms, there are also variant
zipper isomorphisms:
%passes parse
:t #|a :: Iso ({| } | {a:Int | b:Float | c:Unit}) _
(Iso
({ |} | {a: Int32 | b: Float32 | c: Unit})
({a: Int32} | {b: Float32 | c: Unit}))
(MkIso
{fwd=(\v. case v
((Left l)) -> (Left {|a| ...l |})
((Right w)) -> (case w
{| a = x |} -> (Left {| a = x |})
{|a| ...r |} -> (Right r)))
, bwd=(\v. case v
((Left w)) -> (case w
{| a = x |} -> (Right {| a = x |})
{|a| ...r |} -> (Left r))
((Right l)) -> (Right {|a| ...l |}))}
: Iso ((|) { |} {a: Int | b: Float | c: Unit}) _)
split_v makes a prism zipper into an ordinary prism isomorphism:
:t split_v
((a:Type) ?-> Iso a ({ |} | a))
:p
vals : (Fin 3)=>{a:_ | b:_ | c:_ } = [{|a = 1|}, {|b = 2|}, {|c = 3|}]
for i. match_with (split_v &>> #|a &>> #|b) vals.i
[(Just {| a = 1 |}), (Just {| b = 2 |}), Nothing]
slice_fields uses this to specific named variants from a variant-indexed
table:
def abc_to_either {a b c} : Iso {a:a | b:b | c:c} (a|(b|c)) =
fwd = \v. case v of
{|a=x|} -> Left x
{|b=x|} -> Right (Left x)
{|c=x|} -> Right (Right x)
bwd = \v. case v of
Left x -> {|a=x|}
Right x -> case x of
Left y -> {|b=y|}
Right y -> {|c=y|}
MkIso {fwd, bwd}
instance Ix {a:n | b:m | c:q} given {n m q} [Ix n, Ix m, Ix q]
size = size n + size m + size q
ordinal = ordinal <<< app_iso abc_to_either
unsafe_from_ordinal = unsafe_from_ordinal _ >>> rev_iso abc_to_either
def ab_to_either {a b} : Iso {a:a | b:b} (a|b) =
fwd = \v. case v of
{|a=x|} -> Left x
{|b=x|} -> Right x
bwd = \v. case v of
Left x -> {|a=x|}
Right x -> {|b=x|}
MkIso {fwd, bwd}
instance Ix {a:n | b:m} given {n m} [Ix n, Ix m]
size = size n + size m
ordinal = ordinal <<< app_iso ab_to_either
unsafe_from_ordinal = unsafe_from_ordinal _ >>> rev_iso ab_to_either
def ac_to_either {a c} : Iso {a:a | c:c} (a|c) =
fwd = \v. case v of
{|a=x|} -> Left x
{|c=x|} -> Right x
bwd = \v. case v of
Left x -> {|a=x|}
Right x -> {|c=x|}
MkIso {fwd, bwd}
instance Ix {a:n | c:m} given {n m} [Ix n, Ix m]
size = size n + size m
ordinal = ordinal <<< app_iso ac_to_either
unsafe_from_ordinal = unsafe_from_ordinal _ >>> rev_iso ac_to_either
:p
x = iota {a:Fin 2 | b:Fin 2 | c:Fin 2}
v1 = x
v2 = slice_fields (#|a &>> #|b) x
v3 = slice_fields (#|a &>> #|c) x
v4 = slice_fields (#|a &>> #|b &>> #|c) x
(v1, v2, v3, v4)
([0, 1, 2, 3, 4, 5], ([0, 1, 2, 3], ([0, 1, 4, 5], [0, 1, 2, 3, 4, 5])))