Piotr Jander PiotrJander

## mss_dyn_prog.hs
maxSubsetSum :: [Int] -> Int
maxSubsetSum xs = maximum soln
  where
    len = length xs
    arr = listArray (0, len - 1) xs
    go 0 = 0
    go 1 = 0 `max` (arr ! 0)
    go n = (soln ! (n - 1)) `max` ((soln ! (n - 2)) + (arr ! (n - 1)))
    soln = listArray (0, len) [ go i | i <- [0..len] ]

## cake-pattern-counterexample.scala
// Suppose that `ComponentB` requires capabilities `ServiceC` and `ServiceD`,
// and that it internally uses a `ComponentA`. Is there any way `ComponentB`
// can pass its capabilities to `ComponentA`?

trait ServiceC

trait LiveServiceC extends ServiceC

trait ServiceD

## zenhub_issues.html
<html>

<head>
</head>

<body>
  <p>This script has to be run with CORS disabled.
    <a href="https://stackoverflow.com/questions/3102819/disable-same-origin-policy-in-chrome#comment75090678_6083677">
      Instructions for Chrome on MacOS.
    </a>

## moved.html
<ul id="list"><li>luna-studio: <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/12">12</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/13">13</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/14">14</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/15">15</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/16">16</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/30">30</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/32">32</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/33">33</a> <a href="https://app.zenhub.com/workspaces/enso-5b57093c92e09f0d21193695/issues/luna/luna-studio/34">34</a> <a href="https://app.

## akka-websockets.scala
package org.enso

import akka.actor.ActorSystem
import akka.{ Done, NotUsed }
import akka.http.scaladsl.Http
import akka.stream.ActorMaterializer
import akka.stream.scaladsl._
import akka.http.scaladsl.model._
import akka.http.scaladsl.model.ws._
import scala.concurrent.duration._

## State.hs
{-# LANGUAGE InstanceSigs #-}

newtype State s a = State { runState :: s -> (s, a) }

instance Functor (State s) where
  fmap :: (a -> b) -> State s a -> State s b
  fmap f ma = State (fmap f . runState ma)

instance Applicative (State s) where
  pure :: a -> State s a

## Example.scala
import zio.{DefaultRuntime, Task, ZIO}

import scala.io.StdIn

object Example extends App {

  object Console {
    trait Service {
      def getStrLn(): Task[String]
      def putStrLn(s: String): Task[Unit]

## non-zero.agda
module non-zero where

import Data.Vec as V
open V using (Vec; zip; toList)
open V renaming ([] to v[]; _∷_ to _v∷_)
import Data.List as L
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
open L using (List; []; _∷_; filter)
-- open import Data.List.Relation.Binary.Suffix.Heterogeneous
open import Data.Nat -- using (ℕ; zero; suc; _*_; _+_)

## rewriting.agda
-- ...
  where
    xyz : t-to (t-from A') ≡ A'
    xyz = t-to∘from A'
    helper : Δ' T.∋ A'
    helper rewrite sym Δ≡Δ' | xyz = {!S∋→T∋ (ρ x)!}

-- Goal: c-to Δ T.∋ A'
-- Have: c-to Δ T.∋ t-to (t-from A')
-- ————————————————————————————————————————————————————————————

## with-where.agda
Sρ→Tρ : ∀ {Γ Δ}
  → let Γ' = cctx Γ in let Δ' = cctx Δ in
    (∀ {A} → Γ S.∋ A → Δ S.∋ A)
  → T.Renaming Γ' Δ'
Sρ→Tρ {Γ} {Δ} ρ {A'} x with cctx Γ | inspect cctx Γ | cctx Δ | inspect cctx Δ |  ct⁻¹ A' | inspect ct⁻¹ A'
Sρ→Tρ {Γ} {Δ} ρ {A'} x' | Γ' | [ Γ≡Γ' ] | Δ' | [ Δ≡Δ' ] | A | [ A'≡A ] with T∋→S∋ x'
... | x rewrite sym Γ≡Γ' | from∘to Context-iso Γ | xyz = {!S∋→T∋ (ρ x)!}  --  | ct≡ {Conversion.TypeIso.from' A'} | to∘from Type-iso A'
  where
    xyz : ct (Conversion.TypeIso.from' A') ≡ A'
    xyz = to∘from Type-iso A'
	maxSubsetSum :: [Int] -> Int
	maxSubsetSum xs = maximum soln
	where
	len = length xs
	arr = listArray (0, len - 1) xs
	go 0 = 0
	go 1 = 0 `max` (arr ! 0)
	go n = (soln ! (n - 1)) `max` ((soln ! (n - 2)) + (arr ! (n - 1)))
	soln = listArray (0, len) [ go i \| i <- [0..len] ]
	// Suppose that `ComponentB` requires capabilities `ServiceC` and `ServiceD`,
	// and that it internally uses a `ComponentA`. Is there any way `ComponentB`
	// can pass its capabilities to `ComponentA`?

	trait ServiceC

	trait LiveServiceC extends ServiceC

	trait ServiceD
	<html>

	<head>
	</head>

	<body>
	<p>This script has to be run with CORS disabled.
	<a href="https://stackoverflow.com/questions/3102819/disable-same-origin-policy-in-chrome#comment75090678_6083677">
	Instructions for Chrome on MacOS.
	</a>
	package org.enso

	import akka.actor.ActorSystem
	import akka.{ Done, NotUsed }
	import akka.http.scaladsl.Http
	import akka.stream.ActorMaterializer
	import akka.stream.scaladsl._
	import akka.http.scaladsl.model._
	import akka.http.scaladsl.model.ws._
	import scala.concurrent.duration._
	{-# LANGUAGE InstanceSigs #-}

	newtype State s a = State { runState :: s -> (s, a) }

	instance Functor (State s) where
	fmap :: (a -> b) -> State s a -> State s b
	fmap f ma = State (fmap f . runState ma)

	instance Applicative (State s) where
	pure :: a -> State s a
	import zio.{DefaultRuntime, Task, ZIO}

	import scala.io.StdIn

	object Example extends App {

	object Console {
	trait Service {
	def getStrLn(): Task[String]
	def putStrLn(s: String): Task[Unit]
	module non-zero where

	import Data.Vec as V
	open V using (Vec; zip; toList)
	open V renaming ([] to v[]; _∷_ to _v∷_)
	import Data.List as L
	open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
	open L using (List; []; _∷_; filter)
	-- open import Data.List.Relation.Binary.Suffix.Heterogeneous
	open import Data.Nat -- using (ℕ; zero; suc; _*_; _+_)
	-- ...
	where
	xyz : t-to (t-from A') ≡ A'
	xyz = t-to∘from A'
	helper : Δ' T.∋ A'
	helper rewrite sym Δ≡Δ' \| xyz = {!S∋→T∋ (ρ x)!}

	-- Goal: c-to Δ T.∋ A'
	-- Have: c-to Δ T.∋ t-to (t-from A')
	-- ————————————————————————————————————————————————————————————
	Sρ→Tρ : ∀ {Γ Δ}
	→ let Γ' = cctx Γ in let Δ' = cctx Δ in
	(∀ {A} → Γ S.∋ A → Δ S.∋ A)
	→ T.Renaming Γ' Δ'
	Sρ→Tρ {Γ} {Δ} ρ {A'} x with cctx Γ \| inspect cctx Γ \| cctx Δ \| inspect cctx Δ \| ct⁻¹ A' \| inspect ct⁻¹ A'
	Sρ→Tρ {Γ} {Δ} ρ {A'} x' \| Γ' \| [ Γ≡Γ' ] \| Δ' \| [ Δ≡Δ' ] \| A \| [ A'≡A ] with T∋→S∋ x'
	... \| x rewrite sym Γ≡Γ' \| from∘to Context-iso Γ \| xyz = {!S∋→T∋ (ρ x)!} -- \| ct≡ {Conversion.TypeIso.from' A'} \| to∘from Type-iso A'
	where
	xyz : ct (Conversion.TypeIso.from' A') ≡ A'
	xyz = to∘from Type-iso A'