refl 0.1.2

Provides a `refl` encoding which you can use to provide a proof witness that one type is equivalent (identical) to another type. You can use this to encode a subset of what GADTs allow you to in Haskell.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118

# `refl`


[![Build Status](https://travis-ci.org/Centril/refl.svg?branch=master)](https://travis-ci.org/Centril/refl)
[![](http://meritbadge.herokuapp.com/refl)](https://crates.io/crates/refl)

Provides a `refl` encoding which you can use to provide a proof
witness that one type is equivalent (identical) to another type.
You can use this to encode a subset of what GADTs allow you to in Haskell.

This is encoded as:

```rust
use std::mem;
use std::marker::PhantomData;

pub struct Id<S: ?Sized, T: ?Sized>(PhantomData<(*mut S, *mut T)>);

impl<T: ?Sized> Id<T, T> { pub const REFL: Self = Id(PhantomData); }

pub fn refl<T: ?Sized>() -> Id<T, T> { Id::REFL }

impl<S: ?Sized, T: ?Sized> Id<S, T> {
    /// Casts a value of type `S` to `T`.
    ///
    /// This is safe because the `Id` type is always guaranteed to
    /// only be inhabited by `Id<T, T>` types by construction.
    pub fn cast(self, value: S) -> T where S: Sized, T: Sized {
        unsafe {
            // Transmute the value;
            // This is safe since we know by construction that
            // S == T (including lifetime invariance) always holds.
            let cast_value = mem::transmute_copy(&value);
    
            // Forget the value;
            // otherwise the destructor of S would be run.
            mem::forget(value);
    
            cast_value
        }
    }

    // ..
}
```

In Haskell, the `Id<A, B>` type corresponds to:

```haskell
data a :~: b where
    Refl :: a :~: a
```

However, note that you must do the casting manually with `refl.cast(val)`.
Rust will not know that `S == T` by just pattern matching on `Id<S, T>`
(which you can't do).

# Limitations

Please note that Rust has no concept of higher kinded types (HKTs) and so
we can not provide the general transformation `F<S> -> F<T>` given that
`S == T`. With the introduction of generic associated types (GATs), it
may be possible to introduce more transformations.

# Example - A GADT-encoded expression type

```rust
extern crate refl;
use refl::*;

trait Ty { type Repr: Copy + ::std::fmt::Debug; }

#[derive(Debug)]
struct Int;
impl Ty for Int { type Repr = usize; }

#[derive(Debug)]
struct Bool;
impl Ty for Bool { type Repr = bool; }

#[derive(Debug)]
enum Expr<T: Ty> {
    Lit(T::Repr),
    Add(Id<usize, T::Repr>, Box<Expr<Int>>, Box<Expr<Int>>),
    If(Box<Expr<Bool>>, Box<Expr<T>>, Box<Expr<T>>),
}

fn eval<T: Ty>(expr: &Expr<T>) -> T::Repr {
    match *expr {
        Expr::Lit(ref val) =>
            *val,
        Expr::Add(ref refl, ref l, ref r) =>
            refl.cast(eval(&*l) + eval(&*r)),
        Expr::If(ref c, ref i, ref e) =>
            if eval(&*c) { eval(&*i) } else { eval(&*e) },
    }
}

fn main() {
    let expr: Expr<Int> =
        Expr::If(
            Box::new(Expr::Lit(false)),
            Box::new(Expr::Lit(1)),
            Box::new(Expr::Add(
                refl(),
                Box::new(Expr::Lit(2)),
                Box::new(Expr::Lit(3)),
            ))
        );

    assert_eq!(eval(&expr), 5);
}
```

## Contribution


Unless you explicitly state otherwise, any contribution intentionally submitted
for inclusion in the work by you, as defined in the Apache-2.0 license, shall
be dual licensed as above, without any additional terms or conditions.