Monomorphic dynamics without language support

dyn.icl

module dyn

import StdEnv
import Data.Maybe

:: Type
	= Cons String
	| App  Type Type

instance == Type
where
	== (Cons s)  (Cons t)  = s == t
	== (App t u) (App p q) = t == p && u == q
	== _         _         = False

:: Dyn = E.v:
	{ val  :: v
	, type :: Type
	}

class type a :: a -> Type

instance type Int  where type _ = Cons "Int"
instance type Bool where type _ = Cons "Bool"
instance type Char where type _ = Cons "Char"
instance type Real where type _ = Cons "Real"

instance type (a,b) | type a & type b
where
	type t = App (App (Cons "_Tuple2") (type x)) (type y)
	where [(x,y):_] = [undef,t]

instance type [a] | type a
where
	type xs = App (Cons "_List") (type x)
	where [x:_] = [undef:xs]

instance type (a -> b) | type a & type b
where
	type f = App (App (Cons "->") (type i)) (type r)
	where
		i = undef
		[r:_] = [undef,f i]

pack :: a -> Dyn | type a
pack x = {val=x, type=type x}

unpack :: Dyn -> Maybe a | type a
unpack dyn = unpack` undef dyn
where
	unpack` :: a Dyn -> Maybe a | type a
	unpack` x dyn
	| type x == dyn.type = cast Just dyn.val
	| otherwise          = Nothing

	cast :: !u:a -> u:b
	cast _ = code {
		no_op
	}

Start :: Maybe (Int -> Int)
Start = unpack (pack square)

square :: Int -> Int
square x = x * x