This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Control.Monad | |
type Var = Integer | |
type Subst = [(Var, Term)] | |
type State = (Subst, Integer) | |
type Program = State -> KList State | |
data Term = Atom String | Pair Term Term | Var Var deriving Show | |
-- Apply a substitution to the top level of a term |
also posted on http://kyagrd.tumblr.com/post/125748583024/getting-started-with-purescript-0710 Written based on PureScript 0.7.1.0 but shoould work with versions 0.7.0.0 and 0.7.2.0.
PureScript is a purely functional language specifically targeting JavaScript as its backend. If you have tasted Haskell and lamenting about the current untyped mess in scripting languages, especially regarding web-programming, probabiy your only choice out there is PureScript.
PureScript is the only language with a sane approch to staticaly support duck typing on records by using Row Polymorphism.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%%%% Hindley Milner + type constructor polymorphism + rank-1 kind poly | |
use_module(library(apply)). | |
use_module(librar(gensym)). | |
:- set_prolog_flag(occurs_check,true). | |
:- op(500,yfx,$). | |
kind(KC,var(Z),K1) :- first(Z:K,KC), instantiate(K,K1). | |
kind(KC,F $ G, K2) :- kind(KC,F,K1 -> K2), kind(KC,G,K1). | |
kind(KC,A -> B,o) :- kind(KC,A,o), kind(KC,B,o). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --no-positivity-check --no-termination-check #-} | |
module Mendler where | |
open import Data.Bool | |
-- open import Data.Product | |
-- open import Data.String | |
data μ (F : Set → Set) : Set where | |
In : F (μ F) → μ F |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DeriveFunctor, RankNTypes, StandaloneDeriving #-} | |
-- The Glorious Glasgow Haskell Compilation System, version 7.4.1 | |
data F x = C (([x] -> Bool) -> Maybe x) deriving Functor | |
data F1 x = C1 ((forall y . [(y,x)] -> y) -> Maybe x) deriving Functor | |
data F2 x = C2 (forall y . ([x] -> y) -> [(y,x)]) deriving Functor |
NewerOlder