marcoonroad

local prototype = { }
local reason    = { }
local metatable = { }

prototype.erase     = '__please_erase_this_property_in_lookup_rules__'
prototype.protected = true

reason.protected = "Protected against delegated mutation [%s <- %s] by [protected = true]!"
reason.missing   = "No such property/value for selector [%s]!"
reason.mutation  = "Unable to perform property addition/mutation [%s <- %s]!"

marcoonroad

% begin

% --- typing environment ---
% empty context always fails on queries,
% that is, there are unbound variables...

% find :: env * var * type -> prop
find([ type(X, T) | _ ], X, T).

find([ _ | E ], X, T) :-

marcoonroad

package bug;

public class Main {
    public static void main (String[ ] args) {
        SuperClass a = new SuperClass ( ); // 1
        SubClass   b = new SubClass ( );   // 2 e 1.0
        SuperClass c = new SuperClass ( ); // 3
        SubClass   d = new SubClass ( );   // 4 e 2.0

        a.printSelf (c); // 3

marcoonroad

{-# LANGUAGE GADTs #-}

-- dependently typing structures that either does halt or doesn't --

class Natural a where
    natural :: a -> a
    natural = id

class Finite a where
    finite :: a -> a

marcoonroad

-- begin --

local export = { }

local kind = {
  only = 1, all  = 2, any = 3,
  one  = 4, none = 5,
}

local antikind = {

marcoonroad

(* type-level recursion with fold/unfold *)

(* $ eff --effects -l rectypes.eff *)

(* there's an unique isomorphism between fold and unfold such that:

    fold :: ...1 Unfix (...2 Fix (func) ...3) ...4 <=> ...1 Fix (func) ...4 :: unfold
      where func = \fix -> ...2 fix ...3

  so, conceptually:

marcoonroad

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, PolyKinds, KindSignatures, TypeOperators, RankNTypes, UndecidableInstances, AllowAmbiguousTypes, ExistentialQuantification, StandaloneDeriving, UnicodeSyntax, Arrows, MultiParamTypeClasses, ScopedTypeVariables #-}

data Kind = Self
          | Kind `To` Kind

data SingleKind :: Kind -> * where
    SingleSelf :: SingleKind Self
    SingleTo   :: SingleKind a -> SingleKind b -> SingleKind (a `To` b)

instance Show (SingleKind (k :: Kind)) where

marcoonroad

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, GADTs, TypeFamilies, UndecidableInstances #-}

{- about invariants -}
data NatPos = One | Succ NatPos

data SingleNatPos :: NatPos -> * where
    SingleOne  :: SingleNatPos One
    SingleSucc :: SingleNatPos natpos -> SingleNatPos (Succ natpos)

type family (m :: NatPos) |+| (n :: NatPos) :: NatPos where

marcoonroad

-- para matrizes de rank 2 --

-- implementando-as como arvores --
data Tree a = Leaf | Node (Tree a) a (Tree a) deriving Eq

{-

      |                 |
      | A11   A12   A13 |
  a = |                 |

marcoonroad

{-# LANGUAGE GADTs #-}

module Dependent (
    Nat,     O,       S,
    Z,       Zero,    SuccPos, SuccNeg,
    Prop,    V,       X,
    List,    Nil,     Cons,
    Vector,  Exist,   Times,
    Option,  Some,    None,
    Coprod,  OnLeft,  OnRight,