JS.Inheritance

Definitions

interface JSType : Type -> Type

  A `JSType` describes a type's inheritance chains and implemented
  mixins. It is used to safely and conveniently cast a value to a
  less specific type mentioned either in the list of
  mixins or parent types by means of funciton `up` and operator `:>`.

Parameters: a
Methods:

parents : List Type

  The inheritance chain of parent types of this data type
  (starting at the direct supertype). At runtime, such an inheritance
  chain can be inspected by recursively calling the Javascript
  function `Object.getPrototypeOf`.

mixins : List Type

  A Mixin is a concept from WebIDL: It is as programming interface
  shared by several types. Unlike a WebIDL interface, a mixin does
  not describe a type but just set of shared functions and
  attributes. Mixins are not observable by means of inspecting
  a value's prototype chain. It is therefore much harder
  (and right now not supported in this library) to at runtime
  check, whether a value implements a given mixin.

Implementation: 

JSType Object

parents : JSType a => List Type

  The inheritance chain of parent types of this data type
  (starting at the direct supertype). At runtime, such an inheritance
  chain can be inspected by recursively calling the Javascript
  function `Object.getPrototypeOf`.

Totality: total
Visibility: public export

mixins : JSType a => List Type

  A Mixin is a concept from WebIDL: It is as programming interface
  shared by several types. Unlike a WebIDL interface, a mixin does
  not describe a type but just set of shared functions and
  attributes. Mixins are not observable by means of inspecting
  a value's prototype chain. It is therefore much harder
  (and right now not supported in this library) to at runtime
  check, whether a value implements a given mixin.

Totality: total
Visibility: public export

0 Types : (0 a : Type) -> JSType a => List Type

  Convenience alias for `parents`, which takes an explicit
  erased type argument.

Totality: total
Visibility: public export

up : {auto 0 {conArg:2593} : JSType a} -> a -> {auto 0 _ : Elem b (Types a)} -> b

  Safe upcasting. This uses `believe_me` internally and is
  therefore of course only safe, if the `JSType` implementation
  is correct according to some specification and the backend
  properly adhere to this specification.

Totality: total
Visibility: public export

(:>) : {auto 0 {conArg:2619} : JSType a} -> a -> (0 b : Type) -> {auto 0 _ : Elem b (Types a)} -> b

  Operator version of `up`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1

interface SafeCast : Type -> Type

  This is an interface which should be implemented by external
  types, the type of which can be inspected at runtime.
  
  This allows us to at runtime try and safely cast any value
  to the type implementing this interface.
  
  Typically, there are two mechanisms for inspecting a value's
  type at runtime: Function `typeof`, which is mainly useful
  for primitives, and function `unsafeCastOnPrototypeName`, which
  inspects a value's prototype chain
  ([see also](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Inheritance_and_the_prototype_chain)).
  
  Note, that the intention of this interface is to use it
  on *external* types and *primitives*, but not on types
  defined in Idris2. If you need to marshal Idris2 values
  from and to the FFI, use interfaces `ToJS` and `FromJS`.

Parameters: a
Methods:

safeCast : x -> Maybe a

Implementations:

SafeCast JSInt64

SafeCast JSBits64

SafeCast Any

SafeCast Boolean

SafeCast a => SafeCast (Nullable a)

SafeCast Undefined

SafeCast a => SafeCast (UndefOr a)

SafeCast Integer

SafeCast Double

SafeCast String

SafeCast Char

SafeCast Bits8

SafeCast Bits16

SafeCast Bits32

SafeCast Bits64

SafeCast Int8

SafeCast Int16

SafeCast Int32

SafeCast Int64

SafeCast Int

safeCast : SafeCast a => x -> Maybe a

Totality: total
Visibility: public export

castTo : (0 a : Type) -> SafeCast a => x -> Maybe a

Totality: total
Visibility: public export

safeCastAny : All SafeCast ts => x -> Maybe (HSum ts)

  Tries to create an n-ary sum by trying all possible
  casts. The first successful cast will determine the
  result.

Totality: total
Visibility: export

unsafeCastOnPrototypeName : String -> a -> Maybe b

  This is a utility function to implement instances of
  `SafeCast`. Only use, if you know what you are doing.

Totality: total
Visibility: export

unsafeCastOnTypeof : String -> a -> Maybe b

  This is a utility function to implement instances of
  `SafeCast`. Only use, if you know what you are doing.

Totality: total
Visibility: export

bounded : Num a => Integer -> Integer -> x -> Maybe a

Totality: total
Visibility: export

tryCast : SafeCast a => Lazy String -> x -> JSIO a

Totality: total
Visibility: export

tryCast_ : (0 a : Type) -> SafeCast a => Lazy String -> x -> JSIO a

Totality: total
Visibility: export

castingTo : SafeCast a => String -> JSIO x -> JSIO a

Totality: total
Visibility: export