|%
++  diff-type
  |=  =type
  ^+  type
  ::
  ?@  type
    ?-  type
      %noun  -:!>(*(list [axis=@ud new-value=*]))
      %void  ~|  %void-type  !!
    ==
  ?-    -.type
      %atom
    :: constants have no diffs; other atoms are replaced wholesale
    ::
    ?~  constant=q.type
      type
    [%atom %n `~]
  ::
      %cell
    ::
    :+  %cell
      [%face [~ %head] (unit-type $(type p.type))]
    [%face [~ %tail] (unit-type $(type q.type))]
  ::
      %core
    ~|  %core-type  !!
  ::
      %face
    ::
    ?>  ?=(~ p.p.type)
    ?>  ?=(term q.p.type)
    ::
    [%face [~ q.p.type] $(type q.type)]
  ::
      %fork
    ::
    :-  %fork
    %-  ~(run in p.type)
    |=  tine=^type
    ^+  type
    ::
    :-  %fork
    %-  ~(gas in *(set ^type))
    :~  [%cell [%atom %tas `%replace] ^$(type tine)]
        [%cell [%atom %tas `%switch] type(p (~(del in p.type) tine))]
    ==
  ::
      %help
    $(type q.type)  ::  TODO preserve doc
  ::
      %hold
    ::
    :+  %hold
      :+  %cell
        [%face [~ %diff-type-core] -:!>(..diff-type)]
      [%face [~ %played-type] (~(play ut p.type) q.type)]
    ^-  hoon
    [%cnhp [%wing ~[%diff-type %diff-type-core]] [%wing ~[%played-type]]~]
  ==
::  construct a +type for a +unit whose non-nil value is of type :some-type
::
++  unit-type
  |=  some-type=type
  ^-  type
  ::
  :-  %fork
  %-  ~(gas in *(set type))
  ~[nil-type [%cell nil-type [%face [~ %u] some-type]]]
::  convenience arm for a type representing a constant nil
::
++  nil-type  `type`[%atom %n `~]
--