gelisam

At work, I just spent the last few weeks exploring and evaluating every format I could find, and my number one criteria was whether they supported sum types. I was especially interested in schema languages in which I could describe my types and then some standard specifies how to encode them using an on-the-wire format, usually JSON.

1. Swagger represents sum types like Scala does, using subtyping. So you have a parent type EitherIntString with two subtypes Left and Right represented as {"discriminator": "Left", value: 42} and {"discriminator": "Right", value": "foo"}. Unfortunately, unlike in Scala in which the parent type is abstract and cannot be instantiated, in Swagger it looks like the parent type is concrete, so when you specify that your input is an EitherIntString, you might receive {"discriminator": "EitherIntString"} instead of one of its two subtypes.
2. JSON-schema supports unions, which isn't quite the same thing as sum types because

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

{-# OPTIONS --copatterns #-}
module Main where
-- A simple cat program which echoes stdin back to stdout, but implemented using copatterns
-- instead of musical notation, as requested by Miëtek Bak (https://twitter.com/mietek/status/806314271747481600).

open import Data.Nat

open import Data.Unit
open import Data.Bool
open import Data.Char

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

-- 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 response to https://twitter.com/PLT_cheater/status/943901324436963328
{-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes, ScopedTypeVariables #-}
module Main where

import Data.Proxy
import Test.DocTest

-- $setup
-- >>> :set -XDataKinds