Skip to content

Instantly share code, notes, and snippets.

🏠
Working from home

Hiromi Ishii konn

🏠
Working from home
View GitHub Profile
View HKDOpts.hs
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, PolyKinds #-}
{-# LANGUAGE RankNTypes, RecordWildCards, StandaloneDeriving, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Lib where
import Data.Functor.Identity
import Options.Applicative
someFunc :: IO ()
someFunc = putStrLn "someFunc"
View Explosion.hs
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, DeriveDataTypeable, TypeApplications #-}
data Foo (a :: Maybe b) where { Any :: Foo a; Bang :: Foo (Just t) }
newtype F a (t :: Maybe s) (u :: Foo t)
= F { runF :: a} deriving (Show, Eq, Ord, Typeable)
main :: IO ()
main = print $ typeRep $ Proxy @(F Int ('Just ()) Any)
-- ~> No instance for (Typeable (F2 Int ('Just ())))
@konn
konn / monoid.prl
Created Nov 8, 2018
Monoids in RedPRL
View monoid.prl
define IsSemigroup(#ty, #mul) =
(record
[assoc:
(->
[a b c: #ty]
(= #ty
($ #mul a ($ #mul b c))
($ #mul ($ #mul a b) c)
)
)
View ConstraintUnion.hs
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms, RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies, TypeOperators, TypeSynonymInstances #-}
module ConstraintUnion where
import Data.Kind
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Ord
import Data.Type.Equality
import GHC.TypeNats
@konn
konn / lib.rs
Last active Aug 29, 2018
Type-level Peano numerals and sized vectors in Rust (Just for fun)
View lib.rs
use std::marker::PhantomData;
pub trait Nat {
type Eval;
fn as_int() -> usize;
}
#[derive(Debug)]
pub struct Zero {}
@konn
konn / cacher.rs
Last active Aug 17, 2018
Generic Cacher without Clone
View cacher.rs
use std::collections::hash_map::Entry;
use std::collections::HashMap;
use std::hash::Hash;
use std::ops::Fn;
struct Cacher<'a, T, A, B>
where
T: 'a + Fn(&A) -> B,
A: 'a,
B: 'a,
@konn
konn / Cell.hs
Created Jul 18, 2018
Akari (美術館) Solver using SAT solvers
View Cell.hs
{-# LANGUAGE DeriveAnyClass, DeriveDataTypeable, DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies, FlexibleInstances, MultiWayIf #-}
{-# LANGUAGE TypeFamilies #-}
module Cell where
import Control.Applicative (empty)
import Data.Typeable (Typeable)
import Data.Word
import Ersatz
import GHC.Generics (Generic)
@konn
konn / Cell.hs
Created Jul 18, 2018
Akari (美術館) Solver using SAT solvers
View Cell.hs
{-# LANGUAGE DeriveAnyClass, DeriveDataTypeable, DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies, FlexibleInstances, MultiWayIf #-}
{-# LANGUAGE TypeFamilies #-}
module Cell where
import Control.Applicative (empty)
import Data.Typeable (Typeable)
import Data.Word
import Ersatz
import GHC.Generics (Generic)
@konn
konn / Data.Aeson.Generic.DerivingVia.hs
Last active Jun 11, 2020
Type-driven safe derivation of ToJSON and FromJSON, using DerivingVia in GHC 8.6 and some type-level hacks
View Data.Aeson.Generic.DerivingVia.hs
{-# LANGUAGE ConstraintKinds, DataKinds, DeriveGeneric, DerivingVia #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds, ScopedTypeVariables, StandaloneDeriving #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeInType, TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Aeson.Generic.DerivingVia
( StrFun(..), Setting(..), SumEncoding'(..), DefaultOptions, WithOptions(..)
, -- Utility type synonyms to save ticks (') before promoted data constructors
@konn
konn / nix-log.log
Created May 10, 2018
IHaskell compilation failure with Nix on macOS
View nix-log.log
these derivations will be built:
/nix/store/1kg1v5vy0drxyxq66dvvdwkn1304ifh9-qtwebkit-5.9.1.drv
/nix/store/ffja7pc88r4wyfk98pi9nk3yha9adblr-qtwebengine-5.10.1.drv
/nix/store/bzzbb1hrm0dz3rvndyi3mbbxqvyv3mai-python3.6-PyQt-5.10.drv
/nix/store/k8hyi5ys04x3zhskk7hm9sllxxbj4hmh-python3.6-qtconsole-4.3.1.drv
/nix/store/nba4gy75da88hd93gvlq4klq3chjya5m-python3.6-jupyter-1.0.0.drv
/nix/store/asds576kwc2x8zqprh598dvivhnna73b-python3-3.6.5-env.drv
/nix/store/jspp9rcrxh280wnb3l80f820n9hy94bf-ihaskell-console.drv
/nix/store/vas9ys522v10834ysxjb2pzxg4lzacdk-ihaskell-nbconvert.drv
/nix/store/w6hs5ji7dy7j82cw1rh2583ndpn3rgv0-ihaskell-notebook.drv
You can’t perform that action at this time.