bond15

So I'm doing the Lightbend Reactive Arch cert and I'm on module 2 (domain driven design).
The way they talk about 'ubiquitous language' and modeling a domain is very akin to existing work
in Ontology or knowledge representation ( (subject, verb, object) tuple vs (subject, predicate, object) tuple).
(RDF and OWL are not akin to UML)

There are well known tools for managing Ontologies like RDF graphs or the OWL spec language (see Apache Jena).

In fact, I found a paper paper that highlights this similarity 
("An Ontology-based Approach for Domain-driven Design of Microservice Architectures"
https://dl.gi.de/bitstream/handle/20.500.12116/3944/B24-1.pdf?sequence=1)

bond15

open import Data.Nat using (ℕ; _+_; _*_ ; suc)
open import Data.List.Base using (List ; _∷_ ; [] ; map)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; sym; cong)

infixl 20 _⊹_
infixl 19 _⋆_

data ℙ : Set where
  X : ℙ

bond15

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}

-- https://github.com/ekmett/lens/wiki/History-of-Lenses
-- Laarhoven Lenses

-- ghcid -c "ghci Profunctor.hs"


main :: IO ()

bond15

-- 'initial' encoding of object language terms
data Exp = Val Int | Add Exp Exp | Mul Exp Exp

-- 'initial' evaluation of object terms
eval :: Exp -> Int
eval (Val x) = x
eval (Add e1 e2) = (eval e1) + (eval e2)
eval (Mul e1 e2) = (eval e1) * (eval e2)

bond15

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverlappingInstances #-}

data Fix f = In (f (Fix f))

--data Val e = Val e
data IntVal e = Val Int

bond15

module Main where
import Control.Arrow((>>>),(<<<),(&&&),(|||))

{-# LANGUAGE DeriveFunctor #-}


main :: IO ()
main = putStrLn "Hello, Haskell!"

bond15

{-# LANGUAGE GADTs #-}
module Mat where
--import GHC.TypeLits

data Z = Z
data S a = S a

type Zero = Z
type One = S Zero
type Two = S One

bond15

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
module MadLit where
import GHC.TypeNats

bond15

#import "stdio.h"

typedef struct foo {
    int data;
} foo;

typedef struct bar{
    int bla;
    char letter;

bond15

theory Alg
 imports Main
begin 

text‹
  Define algebraic structures as Locales
›
locale monoid =
  fixes M and composition (infixl "⋅" 70) and unit ("𝟭")
  assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"