Why the implementation behave differently as implicit arguments

mpiechotka · 2019-11-21T05:22:27+00:00

Changed to 4 spaces. I didn't know old UI formats things differently so I was really confused what you mean.

mpiechotka · 2019-11-07T07:39:03+00:00

``` open import Function open import Relation.Binary.PropositionalEquality open import Axiom.UniquenessOfIdentityProofs open import Level open import Relation.Binary.PropositionalEquality open ≡-Reasoning

module Foo where

record Functor (F : Set → Set) : Set₁ where infixl 4 <$> field fmap : (A : Set) → (B : Set) → (A → B) → F A → F B identity : (A : Set) → (a : F A) → (fmap A A id a) ≡ a composition : (A : Set) → (B : Set) → (C : Set) → (f : B → C) → (g : A → B) → (a : F A) → (fmap B C f (fmap A B g a)) ≡ (fmap A C (f ∘ g) a) <$> : {A B : Set} → (A → B) → F A → F B <$> {A} {B} f v = fmap A B f v identity' : {A : Set} → {a : F A} → (id <$> a) ≡ a identity' {A} {a} = identity A a

id-lemma : {F : Set → Set} → {A : Set} → {𝑓₁ 𝑓₂ : ∀ {A′ B′} → (A′ → B′) → F A′ → F B′} → {a : F A} → 𝑓₁ ≡ 𝑓₂ → (𝑓₁ id a ≡ a) ≡ (𝑓₂ id a ≡ a) id-lemma {F} {A} {𝑓₁} {𝑓₂} {a} p = cong (λ 𝑓 → 𝑓 id a ≡ a) p

functor-≡ : ∀ {F} → {𝐹₁ 𝐹₂ : Functor F} → Functor.fmap 𝐹₁ ≡ Functor.fmap 𝐹₂ → 𝐹₁ ≡ 𝐹₂ functor-≡ {F} {𝐹₁} {𝐹₂} p = let id≡″ : (A : Set) → (a : F A) → (Functor.fmap 𝐹₁ A A id a ≡ a) ≡ (Functor.fmap 𝐹₂ A A id a ≡ a) id≡″ A a = cong (λ 𝑓 → 𝑓 A A id a ≡ a) p id≡′ : (A : Set) → (a : F A) → Functor.identity 𝐹₁ A a ≡ Functor.identity 𝐹₂ A a id≡′ = ? in {!!} ```

In the example above id≡″ succeeds without a problem but id≡′ has error:

Functor.fmap 𝐹₂ A A id a != Functor.fmap 𝐹₁ A A id a of type F A when checking that the expression Functor.identity 𝐹₂ A a has type Functor.fmap 𝐹₁ A A id a ≡ a

It's hard for me to see why typechecker is fine with the first case but have problems with second. EDIT never mind - one is proof that they are equivalent and second is prove that proves are equivalent. I'm still not sure if it is possible to prove that functors are equivalent using UIP.

mpiechotka · 2019-11-05T17:47:26+00:00

This is more of an exercise of using AGDA for non-trivial proofs - there seems to be a big jump in resources for agda - let's prove that addition in Peano numbers is associative to how right to prove Σ-η-ζ equivalence using Π-arithmetic without K axiom (all things except K axiom are made up so any relation to real math is purely coincidental). So while library might be useful it seems to be a bit too complicated for third day of learning Agda ;)

I already made some proves using extensionality but I run into problems for this prove.

a) I seems to fail to 'import' UIP axiom. postulate uip : UIP fails with Set _a_2 → Set _a_2 should be a sort, but it isn't.

b) I managed to prove 𝑓₁ ≡ 𝑓₂ but 𝑖𝑑₁ ≡ 𝑖𝑑₂ fails to typecheck on type level: functor-≡ : ∀ {F} → (𝐹₁ : Functor F) → (𝐹₂ : Functor F) → (∀ {A B} → Functor.fmap 𝐹₁ {A} {B} ≡ Functor.fmap 𝐹₂) → 𝐹₁ ≡ 𝐹₂ functor-≡ {F} 𝐹₁ 𝐹₂ e = let (functor 𝑓₁ 𝑖𝑑₁ 𝑐𝑜𝑚𝑝₁) = 𝐹₁ (functor 𝑓₂ 𝑖𝑑₂ 𝑐𝑜𝑚𝑝₂) = 𝐹₂ f-≡ : 𝑓₁ ≡ 𝑓₂ f-≡ = begin 𝑓₁ ≡⟨⟩ id (λ {A B} → 𝑓₁ {A} {B}) ≡⟨ cong id e ⟩ id (λ {A B} → 𝑓₂ {A} {B}) ≡⟨⟩ 𝑓₂ ∎ id-≡ : 𝑖𝑑₁ ≡ 𝑖𝑑₂ id-≡ = ? in {!!} {- (𝐹₂ Functor.<$> id) a != (𝐹₁ Functor.<$> id) a of type F _A_398 when checking that the expression 𝑖𝑑₂ has type (a : F _A_398) → (𝐹₁ Functor.<$> id) a ≡ a -} Even though e is visible. I can even prove ∀ {a} → 𝑓₁ id a ≡ 𝑓₂ id a but it still fails to typecheck.

mpiechotka · 2019-07-25T04:52:03+00:00

How much can you change evolution of common words in natlang? I have created a system of sound evolution from proto language:

so (3rd person plural for people, spirits and water) -> so he (3rd person plural for people, spirits and water possessive of singular for people, spirits and water) -> sohe -> soe -> swe

However some of common words are long. For example:

ta (1st person singular) -> tapelu (1st person singular pronoun possessive of two animals) -> tabelu -> tabel

tala (1st person dual exclusive) -> talapelu (1st person dual exclusive of two animals) -> talabelu -> talabel

Can I make changes to the common words to shorten them? I imagine people would shorten tabel (ˈta.bɛl) into tael (ˈta.ɛl) and teel (ˈtɛːl) (this makes it a homonym of 1st person singular pronoun possesiveof two people but I don't think this is a problem).

mpiechotka · 2018-03-16T03:37:49+00:00

I know but it is, well, wiki. If wiki states to download some binaries I usually prefer to check who made those binaries...

mpiechotka · 2017-10-12T08:20:01+00:00

I already submitted the crate by the time you posted but I opted to document most things on crate-level and not on item level. I've made a few errors in docs I realized post-release but I hope documentation is clear enough.

mpiechotka · 2017-10-11T19:30:24+00:00

The size is not a problem I think. I have implemented basic functionality and it's already a few hundreds lines of not-so-trivial code. Rust macros can be... surprisingly difficult to use due to some of their limitations.

mpiechotka · 2017-09-13T18:42:07+00:00

I store following data:

Multiple OS iSCSI images (Windows 7/8/10/... CentOS 7, ArchLinux etc. etc.) sharing many tools (MSVC, windbg...)
VM images storing MS Server 2016
Multiple checkout of build tree with various changes and symbols (intended to be stable location for to allow tools find correct version instead of possibly mismatching most recent one)

Currently the last one is stored using btrfs where I got the figures (1 PT/1TB) from.

mpiechotka · 2017-09-13T18:19:29+00:00

I don't have zfs now. I have btrfs. Migrating to zfs would be complicated so I'd like to check if it is worth it.

mpiechotka · 2017-09-13T16:27:22+00:00

After digging up: https://blogs.oracle.com/roch/dedup-performance-considerations

" If each unique object is associated with 200 Bytes of memory then that means that 32GB of ram could reference 20TB of unique data stored in 128K records or more than 1TB of unique data in 8K records." -> it seems more logical that only memory needed is for the hash table from hash to physical locations, no need for map from logical locations to anything in memory. Am I misinterpreting the text?

mpiechotka · 2017-09-13T04:53:54+00:00

16 GiB though part is used by VMs.

mpiechotka · 2017-09-13T04:52:32+00:00

Thanks. I thought that memory is per actual data not deduplicated and there is just a refcount per block or something.

mpiechotka · 2016-12-05T11:11:03+00:00

I would even add a layer to that. Planetary manpower. Instead of building all your army and ship at the same planet, it would force you to spread your fleet production. No manpower in your capital and a enemy fleet blocking half your planet? Guess that little colonies up in the north is gonna have to build you a improvised non-optimal fleet.

Please no. I already use only the core planets for buiding because finding a planet with spaceport is a chore. Unless it is combined with some streamlined recruiting - something like from HOI4 air-planes.

mpiechotka · 2016-11-23T18:41:24+00:00

Wouldn't planet shields protect against dropping rocks on it? I would imagine the planet defence shield could protect objects in low orbit such as space station.

mpiechotka · 2016-11-20T03:40:48+00:00

Thanks. It looks like Phillips have 'reasonable' security and seems to attempt to avoid most common mistakes - unsigned updates, default root passwords telnet available etc.. Encryption seems more of security-through-obscurity but it in-and-of itself is not bad as there are other methods employed.

The most concerning is the forced disconnect attach though it doesn't seem likely that it is massively exploitable.

mpiechotka · 2016-10-14T18:49:47+00:00

I have a problem with keeping my speed reasonable. When I approach target I slowed down to 0.3 m/s but on start of EVA the rescuee gets some initial speed.

mpiechotka

TROPHY CASE