Basic unit type:
λ> replTy "()"
() :: ()
Basic functions:
{-# OPTIONS_GHC -Wall -fno-warn-incomplete-patterns #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE NPlusKPatterns #-} | |
module Main where |
(ns variant | |
(:require [clojure.core.typed :as t])) | |
(t/defalias V | |
(t/Rec [V] | |
(t/U '[':lambda t/Sym V] | |
'[':if V V V] | |
'[':val t/Any]))) | |
(t/ann command [V -> t/Str]) |
{-# | |
LANGUAGE | |
DeriveGeneric, DeriveDataTypeable, | |
MultiParamTypeClasses, | |
ViewPatterns | |
#-} | |
-- A short example of an ML-style module system atop a core lambda calculus. | |
-- | |
-- The core expression language has variables, applications and | |
-- lambdas and constants. The type language has variables (of the single kind *) |
Basic unit type:
λ> replTy "()"
() :: ()
Basic functions:
At DICOM Grid, we recently made the decision to use Haskell for some of our newer projects, mostly small, independent web services. This isn't the first time I've had the opportunity to use Haskell at work - I had previously used Haskell to write tools to automate some processes like generation of documentation for TypeScript code - but this is the first time we will be deploying Haskell code into production.
Over the past few months, I have been working on two Haskell services:
I will write here mostly about the first project, since it is a self-contained project which provides a good example of the power of Haskell. Moreover, the proces
%default total | |
-- because we're doing proofs | |
-- This file demonstrates a simple example of proof by reflection | |
-- mentioned in: http://ftp.science.ru.nl/CompMath.Found/buchberger.pdf | |
infix 5 <--> | |
(<-->) : Type -> Type -> Type | |
p <--> q = (p -> q, q -> p) |
Warning: Rebar3 works for me, probably won't work for you yet.
Rebar has been an important tool for many years and many Erlang developers, but for various reasons it has come to show it's age very quickly. The code has become overly complex, especially the transitive dependency management, and became clear to me and a few others that a partial rewrite was required.
The prevalence of rebar
configs in projects meant backwards compatability was a must, however features have been both added and removed.
Condensed from: http://comonad.com/reader/2014/letter-to-a-young-haskell-enthusiast/
The following letter is about tendencies that come with the flush of excitement of learning any new thing. It is written specifically, because if we don't talk specifics, the generalities make no sense. It is a letter full of things I want to remember.
You’ve entered the world of strongly typed functional programming, and it is great. You want to share the great things you’ve learned, and you want to slay all the false statements in the world.
module FizzBuzzC | |
%default total | |
-- Dependently typed FizzBuzz, constructively | |
-- A number is fizzy if it is evenly divisible by 3 | |
data Fizzy : Nat -> Type where | |
ZeroFizzy : Fizzy 0 | |
Fizz : Fizzy n -> Fizzy (3 + n) |