UNIQUE t = type {
  type t;
  value : t;
};

Unique () :> UNIQUE () = {
  t = type {};
  value = {};
};

(; You should really use an instance of Unique() with this type.
   or at least another type which is not publically constructable...

   This type does not force that however, for the reason of making it a globally accessible.
   Thus there is no need to accept mk or proj as a parameter anywhere
   and it should not be done since there is no way to preclude 
   others from creating functions with the same type as mk/proj.

   The cost of the above is that to make a globally available instance it must be pure.
   This forces users to pass in Unique values, pushing the effect of unique value generation
   to *outside* of the Trademark.
;)

TRADEMARK = type {
  tm: type => type => type;

  mk 'brand_t 'value_t : brand_t => value_t => tm brand_t value_t;
  proj 'brand_t 'value_t : tm brand_t value_t => value_t;
};

Trademark :> TRADEMARK = {
  tm (_: type) (v: type) = v;
  ;; the following holds: proj o (mk Unique().value) = id
  ;; where mk = flip k.
  mk 'brand_t 'value_t (_: brand_t) (v: value_t) = v;
  proj 'brand_t 'value_t (mark: tm brand_t value_t) = mark : value_t;
};

SEALING 't = type {
  type unsealed = t;
  type sealed;
  type sealer = unsealed => sealed;
  type unsealer = sealed => unsealed;
  

  seal: sealer;
  unseal: unsealer;
};

Sealing t :> SEALING = {
  type unsealed = t;
  type sealed = t;
  (; It is easy to show here that unsealer o sealer = id ;)
  type sealer = unsealed => sealed;
  type unsealer = sealed => unsealed;

  seal v = v;
  unseal v = v;
};

brand = Unique();
foo = Trademark.mk (brand.value) ();
sealing = Sealing (type ());
sealed = sealing.seal ();
() = sealing.unseal sealed;
sealing2 = Sealing (type ());
;; this should however cause a type error...
;; () = sealing2.unseal sealed;


(; There is a silly issue with accepting unseal as a parameter
   from an untrusted party...
  
   assume we have seal: () -> sealed; and unseal: sealed -> ();
   The following function has the same type as an unsealer, but cannot unseal,
   as long as it can construct the return value of ().

   overall a relatively minor act of forgery
   (untested, but note that the composition unsealer o sealer = id does not hold here!).

   sealed_box = sealing.seal ();
   cannot_unseal (_: sealing.sealed) = ();
   foo (unsealer: sealing.sealed) = let unsealed = unsealer sealed_box in ();
   () = foo (cannot_unseal);

   One can either use the above but seal Trademark'ed values,
   or the below which given evidence of a trademark produces trademarked values...
   The latter seems more misuse resistent, in the latter case, 
   you at least need an unsealer or an unsealed value
   in order to produce a function like cannot_unseal.

   This is somewhat reinforced since everyone can share a global Trademark instance,
   which is trusted and has the composition to identity property.
;)

BRANDED_SEALING 'brand_t 't = type {
  type unsealed = Trademark.tm brand_t t;
  type sealed;
  type sealer = t => sealed;
  type unsealer = sealed => unsealed;
  
  seal: sealer;
  unseal: unsealer;
};

BrandedSealing 'brand_t 't (evidence: brand_t)
:> BRANDED_SEALING = {
  type unsealed = Trademark.tm brand_t t;
  type sealed = unsealed;
  type sealer = t => sealed;
  type unsealer = sealed => unsealed;

  seal v = Trademark.mk evidence v;
  unseal v = v;
};

type PRIV_KEY = { type t;  priv : t };
 (; Public key will have just the type portion. ;)
type PUB_KEY = { type t; };
type unit = {};
(; Auth is the type representing a key exchange between 2 parties. ;)
HANDSHAKE t = type {
     ;; The party of the first part.
     type party1_t = t;
     ;; The party of the second part.
     type party2_t;

     ;; signed_t is going to be the return type, the result of a handshake.
     type signed_t = Trademark.tm (type (party2_t, party1_t)) unit;

     ;; a key_observer is provided by the 2nd party
     ;; A function which accepts the first parties private key,
     ;; and returns a signed_t with the first parties private key combined with the 2nd parties own key.
     ;; Note: key_observer_t is pure and cannot abscond with the key.
     type key_observer_t = party1_t => signed_t;   

     ;; handshake_t is provided by the first party,   
     ;; for the 2nd party to call passing their own key_observer_t.
     ;; It then calls key_observer passing in party1_t, (basically its just modus ponens)
     type handshake_t = key_observer_t => signed_t;
};

Handshake (Priv : PRIV_KEY)
          (Base : HANDSHAKE (Priv.t))
: Base.handshake_t  = fun (checkFn : Base.key_observer_t) => checkFn(Priv.priv); 

KeyObserver 'a (Priv : PRIV_KEY)
             (Party1Auth : HANDSHAKE a with (party2_t = Priv.t))  : (Party1Auth.key_observer_t)
  = fun (party1_key : Party1Auth.party1_t) => Trademark.mk (Priv.priv, party1_key) {};

  
(; Curried constructor for the the key exchange type  
   It accepts 1 private key, and one public key.
   In particular it is a large type upon which a Pub.t can be placed.  ;)
Sign (Priv : PRIV_KEY) (Pub : PUB_KEY)
: HANDSHAKE (Priv.t)
 = {
     type party1_t = Priv.t;
     type party2_t = Pub.t;
     type signed_t = Trademark.tm (type (party2_t, party1_t)) unit;
     type key_observer_t = (party1_t => signed_t);
     type handshake_t = key_observer_t => signed_t; 
};

KeyGen() :> PRIV_KEY = {  type t = {};  priv   = {}; };

HandshakeGen() =  let priv_key = KeyGen();  in {
     pub : PUB_KEY = priv_key;
     ;; Partial application expects a PUB_KEY.
     sign = Sign(priv_key);
     key_observer = (KeyObserver priv_key);
     handshake = (Handshake priv_key);
};

Alice = HandshakeGen();
Bob = HandshakeGen();
(; Given the previously applications we perform the handshake ;)
AliceBob = Bob.sign (Alice.pub);
BobAlice = Alice.sign (Bob.pub);
ab = ((Bob.handshake) AliceBob) (Alice.key_observer AliceBob);
ba = ((Alice.handshake) BobAlice) (Bob.key_observer BobAlice);