gelisam

module Main

import Data.Vect

namespace row
  -- (VectD n a i x) is like (xs : Vect n a),
  -- with an extra (x = index' m (toList xs)) index
  data VectD : Nat -> (a : Type) -> Nat -> Maybe a -> Type where
    Nil  : VectD Z a i Nothing
    (::) : (x : a)

gelisam

module Main

import Data.Vect

-- the regular min uses (<) and is not suitable here,
-- we need mymin and diagonal to follow the same recursion pattern
mymin : Nat -> Nat -> Nat
mymin Z y = Z
mymin x Z = Z
mymin (S x) (S y) = S (mymin x y)

gelisam

-- in response to https://gist.github.com/djspiewak/443d37b5d93b92685ce3579cde27b627

-- an example of the problem

data Op a where
  -- returns one row now and a second row later if you want it
  Select :: String -> Op (Row, Prog Row)

type Prog a = Free Op a

gelisam

-- Written in response to https://www.reddit.com/r/dependent_types/comments/51vvvt/is_there_a_way_to_define_a_type_of_homomorphisms/
-- See revision 1 for a less general but easier to understand version
module Homomorphisms where

open import Data.Unit
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Product
open import Relation.Binary.PropositionalEquality

gelisam

-- In response to https://www.reddit.com/r/haskell/comments/54u4lm/trying_fancy_type_stuff_is_it_possible_to_write/
{-# LANGUAGE AllowAmbiguousTypes, DataKinds, FlexibleContexts, GADTs, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeApplications, TypeOperators #-}
module Slice where

import Test.DocTest

-- $setup
-- 
-- Repeating the extensions needed by the tests...
-- 

gelisam

#!/usr/bin/env stack
-- stack --resolver lts-8.16 script

-- for https://www.reddit.com/r/haskell/comments/6emo9g/trying_to_get_the_basic_example_in_cloudhaskell/
{-# LANGUAGE LambdaCase, RecordWildCards #-}
import System.Environment (getArgs)
import Control.Distributed.Process
import Control.Distributed.Process.Node (initRemoteTable)

import Control.Distributed.Process.Backend.SimpleLocalnet

gelisam

-- | A proof of Löb's theorem in Haskell, in reply to [1].
-- 
-- Like Dan Piponi's post on the subject [2], we end up with a function which is
-- basically a spreadsheet evaluator.
-- 
-- Unlike Dan's post, our proof of Löb's theorem follows the Wikipedia
-- proof [3] very closely. Since the proof is using provability logic, we
-- need to encode the rules of provability logic inside Haskell.
-- In particular, we avoid the common mistake of representing the rule
-- 

gelisam

-- in response to https://www.reddit.com/r/haskell/comments/6mz27j/is_it_possible_to_implement_sybstyle/
{-# LANGUAGE ConstraintKinds, DeriveDataTypeable, DeriveGeneric, FlexibleContexts, FlexibleInstances, GADTs, KindSignatures, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TypeApplications, TypeOperators #-}
{-# OPTIONS -Wno-redundant-constraints #-}
module Main where

import Data.Data (Data)
import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable, (:~:)(Refl))
import GHC.Generics (Generic, Rep, U1(..), (:+:)(..), (:*:)(..), K1(..), M1(..))
import Test.DocTest (doctest)

gelisam

-- in reply to http://www.reddit.com/r/haskell/comments/23uzpg/lens_is_unidiomatic_haskell/
-- 
-- What the lens library might look like if Getter, Setter, Fold, Traversal,
-- Lens, Review, and Prism were separate datatypes.
-- 
-- For each optic, I only define enough combinators to explore pairs/sums
-- and lists of integers. Whenever possible, I reimplement the same
-- combinators and the same examples with all optics.

module IdiomaticLens where

gelisam

{-# LANGUAGE DeriveDataTypeable, GADTs, MultiParamTypeClasses, OverloadedStrings, StandaloneDeriving, TypeFamilies #-}
import Control.Applicative
import Control.Monad
import Data.Hashable
import Data.Typeable
import Haxl.Core
import Text.Printf


data E a where